let a, n be Nat; ( 1 <= a implies (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6 )
assume
1 <= a
; (2 |^ (2 |^ n)) + ((6 * a) - 1) > 6
then
6 * 1 <= 6 * a
by XREAL_1:64;
then A1:
(6 * 1) - 1 <= (6 * a) - 1
by XREAL_1:9;
0 + 1 <= 2 |^ n
by NAT_1:13;
then
2 <= 2 |^ (2 |^ n)
by PREPOWER:12;
then
2 + 5 <= (2 |^ (2 |^ n)) + ((6 * a) - 1)
by A1, XREAL_1:7;
hence
(2 |^ (2 |^ n)) + ((6 * a) - 1) > 6
by XXREAL_0:2; verum