Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks4d1p1 Structured version   Visualization version   GIF version

Theorem aks4d1p1 40084
Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 21-Aug-2024.)
Hypotheses
Ref Expression
aks4d1p1.1 (𝜑𝑁 ∈ (ℤ‘3))
aks4d1p1.2 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
aks4d1p1.3 𝐵 = (⌈‘((2 logb 𝑁)↑5))
Assertion
Ref Expression
aks4d1p1 (𝜑𝐴 < (2↑𝐵))
Distinct variable groups:   𝑘,𝑁   𝜑,𝑘
Allowed substitution hints:   𝐴(𝑘)   𝐵(𝑘)

Proof of Theorem aks4d1p1
StepHypRef Expression
1 3nn 12052 . . . . . 6 3 ∈ ℕ
21a1i 11 . . . . 5 ((𝜑 ∧ 3 < 𝑁) → 3 ∈ ℕ)
3 aks4d1p1.1 . . . . . 6 (𝜑𝑁 ∈ (ℤ‘3))
43adantr 481 . . . . 5 ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈ (ℤ‘3))
5 eluznn 12658 . . . . 5 ((3 ∈ ℕ ∧ 𝑁 ∈ (ℤ‘3)) → 𝑁 ∈ ℕ)
62, 4, 5syl2anc 584 . . . 4 ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈ ℕ)
7 aks4d1p1.2 . . . 4 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
8 aks4d1p1.3 . . . 4 𝐵 = (⌈‘((2 logb 𝑁)↑5))
9 3p1e4 12118 . . . . 5 (3 + 1) = 4
10 simpr 485 . . . . . 6 ((𝜑 ∧ 3 < 𝑁) → 3 < 𝑁)
11 3z 12353 . . . . . . . 8 3 ∈ ℤ
1211a1i 11 . . . . . . 7 ((𝜑 ∧ 3 < 𝑁) → 3 ∈ ℤ)
13 eluzelz 12592 . . . . . . . . 9 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
143, 13syl 17 . . . . . . . 8 (𝜑𝑁 ∈ ℤ)
1514adantr 481 . . . . . . 7 ((𝜑 ∧ 3 < 𝑁) → 𝑁 ∈ ℤ)
1612, 15zltp1led 39988 . . . . . 6 ((𝜑 ∧ 3 < 𝑁) → (3 < 𝑁 ↔ (3 + 1) ≤ 𝑁))
1710, 16mpbid 231 . . . . 5 ((𝜑 ∧ 3 < 𝑁) → (3 + 1) ≤ 𝑁)
189, 17eqbrtrrid 5110 . . . 4 ((𝜑 ∧ 3 < 𝑁) → 4 ≤ 𝑁)
19 eqid 2738 . . . 4 (2 logb (((2 logb 𝑁)↑5) + 1)) = (2 logb (((2 logb 𝑁)↑5) + 1))
20 eqid 2738 . . . 4 ((2 logb 𝑁)↑2) = ((2 logb 𝑁)↑2)
21 eqid 2738 . . . 4 ((2 logb 𝑁)↑4) = ((2 logb 𝑁)↑4)
226, 7, 8, 18, 19, 20, 21aks4d1p1p5 40083 . . 3 ((𝜑 ∧ 3 < 𝑁) → 𝐴 < (2↑𝐵))
2322ex 413 . 2 (𝜑 → (3 < 𝑁𝐴 < (2↑𝐵)))
24 simp2 1136 . . . . . . . . . . . 12 ((𝜑 ∧ 3 = 𝑁𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))) → 3 = 𝑁)
2524eqcomd 2744 . . . . . . . . . . 11 ((𝜑 ∧ 3 = 𝑁𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))) → 𝑁 = 3)
2625oveq1d 7290 . . . . . . . . . 10 ((𝜑 ∧ 3 = 𝑁𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))) → (𝑁𝑘) = (3↑𝑘))
2726oveq1d 7290 . . . . . . . . 9 ((𝜑 ∧ 3 = 𝑁𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))) → ((𝑁𝑘) − 1) = ((3↑𝑘) − 1))
28273expa 1117 . . . . . . . 8 (((𝜑 ∧ 3 = 𝑁) ∧ 𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))) → ((𝑁𝑘) − 1) = ((3↑𝑘) − 1))
2928prodeq2dv 15633 . . . . . . 7 ((𝜑 ∧ 3 = 𝑁) → ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((𝑁𝑘) − 1) = ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1))
3029oveq2d 7291 . . . . . 6 ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((𝑁𝑘) − 1)) = ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)))
31 2rp 12735 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ+
3231a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ∈ ℝ+)
33 1red 10976 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℝ)
34 1lt2 12144 . . . . . . . . . . . . . . . . . . 19 1 < 2
3534a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 < 2)
3633, 35ltned 11111 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ≠ 2)
3736necomd 2999 . . . . . . . . . . . . . . . 16 (𝜑 → 2 ≠ 1)
3811a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 3 ∈ ℤ)
3932, 37, 38relogbexpd 39982 . . . . . . . . . . . . . . 15 (𝜑 → (2 logb (2↑3)) = 3)
4039eqcomd 2744 . . . . . . . . . . . . . 14 (𝜑 → 3 = (2 logb (2↑3)))
41 cu2 13917 . . . . . . . . . . . . . . . 16 (2↑3) = 8
4241a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (2↑3) = 8)
4342oveq2d 7291 . . . . . . . . . . . . . 14 (𝜑 → (2 logb (2↑3)) = (2 logb 8))
4440, 43eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → 3 = (2 logb 8))
45 2z 12352 . . . . . . . . . . . . . . 15 2 ∈ ℤ
4645a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℤ)
4746zred 12426 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℝ)
4847leidd 11541 . . . . . . . . . . . . . 14 (𝜑 → 2 ≤ 2)
49 8re 12069 . . . . . . . . . . . . . . 15 8 ∈ ℝ
5049a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 8 ∈ ℝ)
51 8pos 12085 . . . . . . . . . . . . . . 15 0 < 8
5251a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 8)
5332rpgt0d 12775 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 2)
54 3re 12053 . . . . . . . . . . . . . . . . . . 19 3 ∈ ℝ
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 3 ∈ ℝ)
561nngt0i 12012 . . . . . . . . . . . . . . . . . . 19 0 < 3
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 3)
5847, 53, 55, 57, 37relogbcld 39981 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 logb 3) ∈ ℝ)
59 5nn0 12253 . . . . . . . . . . . . . . . . . 18 5 ∈ ℕ0
6059a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 5 ∈ ℕ0)
6158, 60reexpcld 13881 . . . . . . . . . . . . . . . 16 (𝜑 → ((2 logb 3)↑5) ∈ ℝ)
62 ceilcl 13562 . . . . . . . . . . . . . . . 16 (((2 logb 3)↑5) ∈ ℝ → (⌈‘((2 logb 3)↑5)) ∈ ℤ)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℤ)
6463zred 12426 . . . . . . . . . . . . . 14 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℝ)
65 0red 10978 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
66 9re 12072 . . . . . . . . . . . . . . . . 17 9 ∈ ℝ
6766a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 9 ∈ ℝ)
6850lep1d 11906 . . . . . . . . . . . . . . . . 17 (𝜑 → 8 ≤ (8 + 1))
69 8p1e9 12123 . . . . . . . . . . . . . . . . . 18 (8 + 1) = 9
7069a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → (8 + 1) = 9)
7168, 70breqtrd 5100 . . . . . . . . . . . . . . . 16 (𝜑 → 8 ≤ 9)
72 2re 12047 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℝ
7372a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 2 ∈ ℝ)
74 2pos 12076 . . . . . . . . . . . . . . . . . . . 20 0 < 2
7574a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 2)
76 3pos 12078 . . . . . . . . . . . . . . . . . . . 20 0 < 3
7776a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 < 3)
7873, 75, 55, 77, 37relogbcld 39981 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2 logb 3) ∈ ℝ)
7978, 60reexpcld 13881 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 logb 3)↑5) ∈ ℝ)
8079, 62syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℤ)
8180zred 12426 . . . . . . . . . . . . . . . . 17 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℝ)
8255leidd 11541 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 3 ≤ 3)
8355, 823lexlogpow5ineq4 40064 . . . . . . . . . . . . . . . . . 18 (𝜑 → 9 < ((2 logb 3)↑5))
8467, 79, 83ltled 11123 . . . . . . . . . . . . . . . . 17 (𝜑 → 9 ≤ ((2 logb 3)↑5))
85 ceilge 13565 . . . . . . . . . . . . . . . . . 18 (((2 logb 3)↑5) ∈ ℝ → ((2 logb 3)↑5) ≤ (⌈‘((2 logb 3)↑5)))
8679, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 logb 3)↑5) ≤ (⌈‘((2 logb 3)↑5)))
8767, 79, 81, 84, 86letrd 11132 . . . . . . . . . . . . . . . 16 (𝜑 → 9 ≤ (⌈‘((2 logb 3)↑5)))
8850, 67, 64, 71, 87letrd 11132 . . . . . . . . . . . . . . 15 (𝜑 → 8 ≤ (⌈‘((2 logb 3)↑5)))
8965, 50, 64, 52, 88ltletrd 11135 . . . . . . . . . . . . . 14 (𝜑 → 0 < (⌈‘((2 logb 3)↑5)))
9046, 48, 50, 52, 64, 89, 88logblebd 39984 . . . . . . . . . . . . 13 (𝜑 → (2 logb 8) ≤ (2 logb (⌈‘((2 logb 3)↑5))))
9144, 90eqbrtrd 5096 . . . . . . . . . . . 12 (𝜑 → 3 ≤ (2 logb (⌈‘((2 logb 3)↑5))))
9279, 33readdcld 11004 . . . . . . . . . . . . . . . 16 (𝜑 → (((2 logb 3)↑5) + 1) ∈ ℝ)
93 1nn0 12249 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ0
94 6nn 12062 . . . . . . . . . . . . . . . . . . 19 6 ∈ ℕ
9593, 94decnncl 12457 . . . . . . . . . . . . . . . . . 18 16 ∈ ℕ
9695a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑16 ∈ ℕ)
9796nnred 11988 . . . . . . . . . . . . . . . 16 (𝜑16 ∈ ℝ)
98 ceilm1lt 13568 . . . . . . . . . . . . . . . . . 18 (((2 logb 3)↑5) ∈ ℝ → ((⌈‘((2 logb 3)↑5)) − 1) < ((2 logb 3)↑5))
9979, 98syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌈‘((2 logb 3)↑5)) − 1) < ((2 logb 3)↑5))
10081, 33, 79ltsubaddd 11571 . . . . . . . . . . . . . . . . 17 (𝜑 → (((⌈‘((2 logb 3)↑5)) − 1) < ((2 logb 3)↑5) ↔ (⌈‘((2 logb 3)↑5)) < (((2 logb 3)↑5) + 1)))
10199, 100mpbid 231 . . . . . . . . . . . . . . . 16 (𝜑 → (⌈‘((2 logb 3)↑5)) < (((2 logb 3)↑5) + 1))
102 3lexlogpow5ineq5 40068 . . . . . . . . . . . . . . . . . . 19 ((2 logb 3)↑5) ≤ 15
103102a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2 logb 3)↑5) ≤ 15)
104 5p1e6 12120 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 1) = 6
105 eqid 2738 . . . . . . . . . . . . . . . . . . . . . 22 15 = 15
10693, 59, 104, 105decsuc 12468 . . . . . . . . . . . . . . . . . . . . 21 (15 + 1) = 16
107106a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (15 + 1) = 16)
10897recnd 11003 . . . . . . . . . . . . . . . . . . . . 21 (𝜑16 ∈ ℂ)
109 1cnd 10970 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ∈ ℂ)
110 5nn 12059 . . . . . . . . . . . . . . . . . . . . . . . 24 5 ∈ ℕ
11193, 110decnncl 12457 . . . . . . . . . . . . . . . . . . . . . . 23 15 ∈ ℕ
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑15 ∈ ℕ)
113112nncnd 11989 . . . . . . . . . . . . . . . . . . . . 21 (𝜑15 ∈ ℂ)
114108, 109, 113subadd2d 11351 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((16 − 1) = 15 ↔ (15 + 1) = 16))
115107, 114mpbird 256 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (16 − 1) = 15)
116115eqcomd 2744 . . . . . . . . . . . . . . . . . 18 (𝜑15 = (16 − 1))
117103, 116breqtrd 5100 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 logb 3)↑5) ≤ (16 − 1))
118 leaddsub 11451 . . . . . . . . . . . . . . . . . 18 ((((2 logb 3)↑5) ∈ ℝ ∧ 1 ∈ ℝ ∧ 16 ∈ ℝ) → ((((2 logb 3)↑5) + 1) ≤ 16 ↔ ((2 logb 3)↑5) ≤ (16 − 1)))
11979, 33, 97, 118syl3anc 1370 . . . . . . . . . . . . . . . . 17 (𝜑 → ((((2 logb 3)↑5) + 1) ≤ 16 ↔ ((2 logb 3)↑5) ≤ (16 − 1)))
120117, 119mpbird 256 . . . . . . . . . . . . . . . 16 (𝜑 → (((2 logb 3)↑5) + 1) ≤ 16)
12181, 92, 97, 101, 120ltletrd 11135 . . . . . . . . . . . . . . 15 (𝜑 → (⌈‘((2 logb 3)↑5)) < 16)
122 eqid 2738 . . . . . . . . . . . . . . . . 17 16 = 16
123 2exp4 16786 . . . . . . . . . . . . . . . . 17 (2↑4) = 16
124122, 123eqtr4i 2769 . . . . . . . . . . . . . . . 16 16 = (2↑4)
125124a1i 11 . . . . . . . . . . . . . . 15 (𝜑16 = (2↑4))
126121, 125breqtrd 5100 . . . . . . . . . . . . . 14 (𝜑 → (⌈‘((2 logb 3)↑5)) < (2↑4))
12746uzidd 12598 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ (ℤ‘2))
12864, 89elrpd 12769 . . . . . . . . . . . . . . 15 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℝ+)
129 4z 12354 . . . . . . . . . . . . . . . . 17 4 ∈ ℤ
130129a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 4 ∈ ℤ)
13132, 130rpexpcld 13962 . . . . . . . . . . . . . . 15 (𝜑 → (2↑4) ∈ ℝ+)
132 logblt 25934 . . . . . . . . . . . . . . 15 ((2 ∈ (ℤ‘2) ∧ (⌈‘((2 logb 3)↑5)) ∈ ℝ+ ∧ (2↑4) ∈ ℝ+) → ((⌈‘((2 logb 3)↑5)) < (2↑4) ↔ (2 logb (⌈‘((2 logb 3)↑5))) < (2 logb (2↑4))))
133127, 128, 131, 132syl3anc 1370 . . . . . . . . . . . . . 14 (𝜑 → ((⌈‘((2 logb 3)↑5)) < (2↑4) ↔ (2 logb (⌈‘((2 logb 3)↑5))) < (2 logb (2↑4))))
134126, 133mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (2 logb (⌈‘((2 logb 3)↑5))) < (2 logb (2↑4)))
13532, 37, 130relogbexpd 39982 . . . . . . . . . . . . . 14 (𝜑 → (2 logb (2↑4)) = 4)
1369eqcomi 2747 . . . . . . . . . . . . . . 15 4 = (3 + 1)
137136a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 4 = (3 + 1))
138135, 137eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → (2 logb (2↑4)) = (3 + 1))
139134, 138breqtrd 5100 . . . . . . . . . . . 12 (𝜑 → (2 logb (⌈‘((2 logb 3)↑5))) < (3 + 1))
14091, 139jca 512 . . . . . . . . . . 11 (𝜑 → (3 ≤ (2 logb (⌈‘((2 logb 3)↑5))) ∧ (2 logb (⌈‘((2 logb 3)↑5))) < (3 + 1)))
14173, 75, 55, 57, 37relogbcld 39981 . . . . . . . . . . . . . . . 16 (𝜑 → (2 logb 3) ∈ ℝ)
142141, 60reexpcld 13881 . . . . . . . . . . . . . . 15 (𝜑 → ((2 logb 3)↑5) ∈ ℝ)
143142, 62syl 17 . . . . . . . . . . . . . 14 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℤ)
144143zred 12426 . . . . . . . . . . . . 13 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℝ)
145 9pos 12086 . . . . . . . . . . . . . . 15 0 < 9
146145a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 9)
14765, 67, 144, 146, 87ltletrd 11135 . . . . . . . . . . . . 13 (𝜑 → 0 < (⌈‘((2 logb 3)↑5)))
14873, 75, 144, 147, 37relogbcld 39981 . . . . . . . . . . . 12 (𝜑 → (2 logb (⌈‘((2 logb 3)↑5))) ∈ ℝ)
149 flbi 13536 . . . . . . . . . . . 12 (((2 logb (⌈‘((2 logb 3)↑5))) ∈ ℝ ∧ 3 ∈ ℤ) → ((⌊‘(2 logb (⌈‘((2 logb 3)↑5)))) = 3 ↔ (3 ≤ (2 logb (⌈‘((2 logb 3)↑5))) ∧ (2 logb (⌈‘((2 logb 3)↑5))) < (3 + 1))))
150148, 38, 149syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((⌊‘(2 logb (⌈‘((2 logb 3)↑5)))) = 3 ↔ (3 ≤ (2 logb (⌈‘((2 logb 3)↑5))) ∧ (2 logb (⌈‘((2 logb 3)↑5))) < (3 + 1))))
151140, 150mpbird 256 . . . . . . . . . 10 (𝜑 → (⌊‘(2 logb (⌈‘((2 logb 3)↑5)))) = 3)
152151oveq2d 7291 . . . . . . . . 9 (𝜑 → (3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) = (3↑3))
15378resqcld 13965 . . . . . . . . . . . . . . 15 (𝜑 → ((2 logb 3)↑2) ∈ ℝ)
154 3lexlogpow2ineq2 40067 . . . . . . . . . . . . . . . . 17 (2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3)
155154a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (2 < ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < 3))
156155simpld 495 . . . . . . . . . . . . . . 15 (𝜑 → 2 < ((2 logb 3)↑2))
15773, 153, 156ltled 11123 . . . . . . . . . . . . . 14 (𝜑 → 2 ≤ ((2 logb 3)↑2))
158155simprd 496 . . . . . . . . . . . . . . 15 (𝜑 → ((2 logb 3)↑2) < 3)
159 df-3 12037 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
160159a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 3 = (2 + 1))
161158, 160breqtrd 5100 . . . . . . . . . . . . . 14 (𝜑 → ((2 logb 3)↑2) < (2 + 1))
162157, 161jca 512 . . . . . . . . . . . . 13 (𝜑 → (2 ≤ ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < (2 + 1)))
163141resqcld 13965 . . . . . . . . . . . . . 14 (𝜑 → ((2 logb 3)↑2) ∈ ℝ)
164 flbi 13536 . . . . . . . . . . . . . 14 ((((2 logb 3)↑2) ∈ ℝ ∧ 2 ∈ ℤ) → ((⌊‘((2 logb 3)↑2)) = 2 ↔ (2 ≤ ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < (2 + 1))))
165163, 46, 164syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → ((⌊‘((2 logb 3)↑2)) = 2 ↔ (2 ≤ ((2 logb 3)↑2) ∧ ((2 logb 3)↑2) < (2 + 1))))
166162, 165mpbird 256 . . . . . . . . . . . 12 (𝜑 → (⌊‘((2 logb 3)↑2)) = 2)
167166oveq2d 7291 . . . . . . . . . . 11 (𝜑 → (1...(⌊‘((2 logb 3)↑2))) = (1...2))
168167prodeq1d 15631 . . . . . . . . . 10 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1) = ∏𝑘 ∈ (1...2)((3↑𝑘) − 1))
169 1zzd 12351 . . . . . . . . . . . . . 14 (𝜑 → 1 ∈ ℤ)
170169, 46jca 512 . . . . . . . . . . . . 13 (𝜑 → (1 ∈ ℤ ∧ 2 ∈ ℤ))
171 1le2 12182 . . . . . . . . . . . . . . 15 1 ≤ 2
172171a1i 11 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 2 ∈ ℤ) → 1 ≤ 2)
173 eluz 12596 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ 2 ∈ ℤ) → (2 ∈ (ℤ‘1) ↔ 1 ≤ 2))
174172, 173mpbird 256 . . . . . . . . . . . . 13 ((1 ∈ ℤ ∧ 2 ∈ ℤ) → 2 ∈ (ℤ‘1))
175170, 174syl 17 . . . . . . . . . . . 12 (𝜑 → 2 ∈ (ℤ‘1))
176 3cn 12054 . . . . . . . . . . . . . . 15 3 ∈ ℂ
177176a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...2)) → 3 ∈ ℂ)
178 elfznn 13285 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (1...2) → 𝑘 ∈ ℕ)
179178adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ)
180179nnnn0d 12293 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ0)
181177, 180expcld 13864 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...2)) → (3↑𝑘) ∈ ℂ)
182 1cnd 10970 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (1...2)) → 1 ∈ ℂ)
183181, 182subcld 11332 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (1...2)) → ((3↑𝑘) − 1) ∈ ℂ)
184 oveq2 7283 . . . . . . . . . . . . 13 (𝑘 = 2 → (3↑𝑘) = (3↑2))
185184oveq1d 7290 . . . . . . . . . . . 12 (𝑘 = 2 → ((3↑𝑘) − 1) = ((3↑2) − 1))
186175, 183, 185fprodm1 15677 . . . . . . . . . . 11 (𝜑 → ∏𝑘 ∈ (1...2)((3↑𝑘) − 1) = (∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) · ((3↑2) − 1)))
187 2m1e1 12099 . . . . . . . . . . . . . . . 16 (2 − 1) = 1
188187a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (2 − 1) = 1)
189188oveq2d 7291 . . . . . . . . . . . . . 14 (𝜑 → (1...(2 − 1)) = (1...1))
190189prodeq1d 15631 . . . . . . . . . . . . 13 (𝜑 → ∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) = ∏𝑘 ∈ (1...1)((3↑𝑘) − 1))
19155recnd 11003 . . . . . . . . . . . . . . . . 17 (𝜑 → 3 ∈ ℂ)
19293a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℕ0)
193191, 192expcld 13864 . . . . . . . . . . . . . . . 16 (𝜑 → (3↑1) ∈ ℂ)
194193, 109subcld 11332 . . . . . . . . . . . . . . 15 (𝜑 → ((3↑1) − 1) ∈ ℂ)
195169, 194jca 512 . . . . . . . . . . . . . 14 (𝜑 → (1 ∈ ℤ ∧ ((3↑1) − 1) ∈ ℂ))
196 oveq2 7283 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → (3↑𝑘) = (3↑1))
197196oveq1d 7290 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ((3↑𝑘) − 1) = ((3↑1) − 1))
198197fprod1 15673 . . . . . . . . . . . . . 14 ((1 ∈ ℤ ∧ ((3↑1) − 1) ∈ ℂ) → ∏𝑘 ∈ (1...1)((3↑𝑘) − 1) = ((3↑1) − 1))
199195, 198syl 17 . . . . . . . . . . . . 13 (𝜑 → ∏𝑘 ∈ (1...1)((3↑𝑘) − 1) = ((3↑1) − 1))
200190, 199eqtrd 2778 . . . . . . . . . . . 12 (𝜑 → ∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) = ((3↑1) − 1))
201200oveq1d 7290 . . . . . . . . . . 11 (𝜑 → (∏𝑘 ∈ (1...(2 − 1))((3↑𝑘) − 1) · ((3↑2) − 1)) = (((3↑1) − 1) · ((3↑2) − 1)))
202186, 201eqtrd 2778 . . . . . . . . . 10 (𝜑 → ∏𝑘 ∈ (1...2)((3↑𝑘) − 1) = (((3↑1) − 1) · ((3↑2) − 1)))
203168, 202eqtrd 2778 . . . . . . . . 9 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1) = (((3↑1) − 1) · ((3↑2) − 1)))
204152, 203oveq12d 7293 . . . . . . . 8 (𝜑 → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) = ((3↑3) · (((3↑1) − 1) · ((3↑2) − 1))))
205 3nn0 12251 . . . . . . . . . . . 12 3 ∈ ℕ0
206205a1i 11 . . . . . . . . . . 11 (𝜑 → 3 ∈ ℕ0)
20755, 206reexpcld 13881 . . . . . . . . . 10 (𝜑 → (3↑3) ∈ ℝ)
20855, 192reexpcld 13881 . . . . . . . . . . . 12 (𝜑 → (3↑1) ∈ ℝ)
209208, 33resubcld 11403 . . . . . . . . . . 11 (𝜑 → ((3↑1) − 1) ∈ ℝ)
21055resqcld 13965 . . . . . . . . . . . 12 (𝜑 → (3↑2) ∈ ℝ)
211210, 33resubcld 11403 . . . . . . . . . . 11 (𝜑 → ((3↑2) − 1) ∈ ℝ)
212209, 211remulcld 11005 . . . . . . . . . 10 (𝜑 → (((3↑1) − 1) · ((3↑2) − 1)) ∈ ℝ)
213207, 212remulcld 11005 . . . . . . . . 9 (𝜑 → ((3↑3) · (((3↑1) − 1) · ((3↑2) − 1))) ∈ ℝ)
214 9nn0 12257 . . . . . . . . . . . 12 9 ∈ ℕ0
215214a1i 11 . . . . . . . . . . 11 (𝜑 → 9 ∈ ℕ0)
21673, 215reexpcld 13881 . . . . . . . . . 10 (𝜑 → (2↑9) ∈ ℝ)
217216, 33resubcld 11403 . . . . . . . . 9 (𝜑 → ((2↑9) − 1) ∈ ℝ)
218 elnnz 12329 . . . . . . . . . . . . 13 ((⌈‘((2 logb 3)↑5)) ∈ ℕ ↔ ((⌈‘((2 logb 3)↑5)) ∈ ℤ ∧ 0 < (⌈‘((2 logb 3)↑5))))
219143, 147, 218sylanbrc 583 . . . . . . . . . . . 12 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℕ)
220219orcd 870 . . . . . . . . . . 11 (𝜑 → ((⌈‘((2 logb 3)↑5)) ∈ ℕ ∨ (⌈‘((2 logb 3)↑5)) = 0))
221 elnn0 12235 . . . . . . . . . . . 12 ((⌈‘((2 logb 3)↑5)) ∈ ℕ0 ↔ ((⌈‘((2 logb 3)↑5)) ∈ ℕ ∨ (⌈‘((2 logb 3)↑5)) = 0))
222221a1i 11 . . . . . . . . . . 11 (𝜑 → ((⌈‘((2 logb 3)↑5)) ∈ ℕ0 ↔ ((⌈‘((2 logb 3)↑5)) ∈ ℕ ∨ (⌈‘((2 logb 3)↑5)) = 0)))
223220, 222mpbird 256 . . . . . . . . . 10 (𝜑 → (⌈‘((2 logb 3)↑5)) ∈ ℕ0)
22473, 223reexpcld 13881 . . . . . . . . 9 (𝜑 → (2↑(⌈‘((2 logb 3)↑5))) ∈ ℝ)
225 8cn 12070 . . . . . . . . . . . . . . 15 8 ∈ ℂ
226 2cn 12048 . . . . . . . . . . . . . . 15 2 ∈ ℂ
227 8t2e16 12552 . . . . . . . . . . . . . . 15 (8 · 2) = 16
228225, 226, 227mulcomli 10984 . . . . . . . . . . . . . 14 (2 · 8) = 16
229228a1i 11 . . . . . . . . . . . . 13 (𝜑 → (2 · 8) = 16)
230229oveq2d 7291 . . . . . . . . . . . 12 (𝜑 → (27 · (2 · 8)) = (27 · 16))
231 6nn0 12254 . . . . . . . . . . . . . . 15 6 ∈ ℕ0
23293, 231deccl 12452 . . . . . . . . . . . . . 14 16 ∈ ℕ0
233 2nn0 12250 . . . . . . . . . . . . . 14 2 ∈ ℕ0
234 7nn0 12255 . . . . . . . . . . . . . 14 7 ∈ ℕ0
235 eqid 2738 . . . . . . . . . . . . . 14 27 = 27
23693, 93deccl 12452 . . . . . . . . . . . . . 14 11 ∈ ℕ0
237 0nn0 12248 . . . . . . . . . . . . . . 15 0 ∈ ℕ0
238233dec0h 12459 . . . . . . . . . . . . . . 15 2 = 02
239 eqid 2738 . . . . . . . . . . . . . . 15 11 = 11
240232nn0cni 12245 . . . . . . . . . . . . . . . . . 18 16 ∈ ℂ
241240mul02i 11164 . . . . . . . . . . . . . . . . 17 (0 · 16) = 0
242 ax-1cn 10929 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
243176, 242, 9addcomli 11167 . . . . . . . . . . . . . . . . 17 (1 + 3) = 4
244241, 243oveq12i 7287 . . . . . . . . . . . . . . . 16 ((0 · 16) + (1 + 3)) = (0 + 4)
245 4cn 12058 . . . . . . . . . . . . . . . . 17 4 ∈ ℂ
246245addid2i 11163 . . . . . . . . . . . . . . . 16 (0 + 4) = 4
247244, 246eqtri 2766 . . . . . . . . . . . . . . 15 ((0 · 16) + (1 + 3)) = 4
24893dec0h 12459 . . . . . . . . . . . . . . . 16 1 = 01
249 2t1e2 12136 . . . . . . . . . . . . . . . . . 18 (2 · 1) = 2
250 0p1e1 12095 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
251249, 250oveq12i 7287 . . . . . . . . . . . . . . . . 17 ((2 · 1) + (0 + 1)) = (2 + 1)
252 2p1e3 12115 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
253251, 252eqtri 2766 . . . . . . . . . . . . . . . 16 ((2 · 1) + (0 + 1)) = 3
254 6cn 12064 . . . . . . . . . . . . . . . . . 18 6 ∈ ℂ
255 6t2e12 12541 . . . . . . . . . . . . . . . . . 18 (6 · 2) = 12
256254, 226, 255mulcomli 10984 . . . . . . . . . . . . . . . . 17 (2 · 6) = 12
25793, 233, 252, 256decsuc 12468 . . . . . . . . . . . . . . . 16 ((2 · 6) + 1) = 13
25893, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257decma2c 12490 . . . . . . . . . . . . . . 15 ((2 · 16) + 1) = 33
259237, 233, 93, 93, 238, 239, 232, 205, 205, 247, 258decmac 12489 . . . . . . . . . . . . . 14 ((2 · 16) + 11) = 43
260 4nn0 12252 . . . . . . . . . . . . . . 15 4 ∈ ℕ0
261 7cn 12067 . . . . . . . . . . . . . . . . . 18 7 ∈ ℂ
262261mulid1i 10979 . . . . . . . . . . . . . . . . 17 (7 · 1) = 7
263262oveq1i 7285 . . . . . . . . . . . . . . . 16 ((7 · 1) + 4) = (7 + 4)
264 7p4e11 12513 . . . . . . . . . . . . . . . 16 (7 + 4) = 11
265263, 264eqtri 2766 . . . . . . . . . . . . . . 15 ((7 · 1) + 4) = 11
266 7t6e42 12550 . . . . . . . . . . . . . . 15 (7 · 6) = 42
267234, 93, 231, 122, 233, 260, 265, 266decmul2c 12503 . . . . . . . . . . . . . 14 (7 · 16) = 112
268232, 233, 234, 235, 233, 236, 259, 267decmul1c 12502 . . . . . . . . . . . . 13 (27 · 16) = 432
269268a1i 11 . . . . . . . . . . . 12 (𝜑 → (27 · 16) = 432)
270230, 269eqtrd 2778 . . . . . . . . . . 11 (𝜑 → (27 · (2 · 8)) = 432)
271260, 205deccl 12452 . . . . . . . . . . . . 13 43 ∈ ℕ0
27259, 93deccl 12452 . . . . . . . . . . . . 13 51 ∈ ℕ0
273 2lt10 12575 . . . . . . . . . . . . 13 2 < 10
274 3lt10 12574 . . . . . . . . . . . . . 14 3 < 10
275 4lt5 12150 . . . . . . . . . . . . . 14 4 < 5
276260, 59, 205, 93, 274, 275decltc 12466 . . . . . . . . . . . . 13 43 < 51
277271, 272, 233, 93, 273, 276decltc 12466 . . . . . . . . . . . 12 432 < 511
278277a1i 11 . . . . . . . . . . 11 (𝜑432 < 511)
279270, 278eqbrtrd 5096 . . . . . . . . . 10 (𝜑 → (27 · (2 · 8)) < 511)
280 3exp3 16793 . . . . . . . . . . . . 13 (3↑3) = 27
281280a1i 11 . . . . . . . . . . . 12 (𝜑 → (3↑3) = 27)
282281eqcomd 2744 . . . . . . . . . . 11 (𝜑27 = (3↑3))
283191exp1d 13859 . . . . . . . . . . . . . 14 (𝜑 → (3↑1) = 3)
284283oveq1d 7290 . . . . . . . . . . . . 13 (𝜑 → ((3↑1) − 1) = (3 − 1))
285 3m1e2 12101 . . . . . . . . . . . . . 14 (3 − 1) = 2
286285a1i 11 . . . . . . . . . . . . 13 (𝜑 → (3 − 1) = 2)
287284, 286eqtr2d 2779 . . . . . . . . . . . 12 (𝜑 → 2 = ((3↑1) − 1))
288 sq3 13915 . . . . . . . . . . . . . . 15 (3↑2) = 9
289288a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (3↑2) = 9)
290289oveq1d 7290 . . . . . . . . . . . . 13 (𝜑 → ((3↑2) − 1) = (9 − 1))
291 9m1e8 12107 . . . . . . . . . . . . . 14 (9 − 1) = 8
292291a1i 11 . . . . . . . . . . . . 13 (𝜑 → (9 − 1) = 8)
293290, 292eqtr2d 2779 . . . . . . . . . . . 12 (𝜑 → 8 = ((3↑2) − 1))
294287, 293oveq12d 7293 . . . . . . . . . . 11 (𝜑 → (2 · 8) = (((3↑1) − 1) · ((3↑2) − 1)))
295282, 294oveq12d 7293 . . . . . . . . . 10 (𝜑 → (27 · (2 · 8)) = ((3↑3) · (((3↑1) − 1) · ((3↑2) − 1))))
296 df-9 12043 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
297296a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 9 = (8 + 1))
298297oveq2d 7291 . . . . . . . . . . . . . 14 (𝜑 → (2↑9) = (2↑(8 + 1)))
299287, 194eqeltrd 2839 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
300 8nn0 12256 . . . . . . . . . . . . . . . 16 8 ∈ ℕ0
301300a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 8 ∈ ℕ0)
302299, 192, 301expaddd 13866 . . . . . . . . . . . . . 14 (𝜑 → (2↑(8 + 1)) = ((2↑8) · (2↑1)))
303298, 302eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → (2↑9) = ((2↑8) · (2↑1)))
304 2exp8 16790 . . . . . . . . . . . . . . . . 17 (2↑8) = 256
305304a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑8) = 256)
306305oveq1d 7290 . . . . . . . . . . . . . . 15 (𝜑 → ((2↑8) · (2↑1)) = (256 · (2↑1)))
307299exp1d 13859 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑1) = 2)
308307oveq2d 7291 . . . . . . . . . . . . . . 15 (𝜑 → (256 · (2↑1)) = (256 · 2))
309306, 308eqtrd 2778 . . . . . . . . . . . . . 14 (𝜑 → ((2↑8) · (2↑1)) = (256 · 2))
310233, 59deccl 12452 . . . . . . . . . . . . . . . 16 25 ∈ ℕ0
311 eqid 2738 . . . . . . . . . . . . . . . 16 256 = 256
312 eqid 2738 . . . . . . . . . . . . . . . . 17 25 = 25
313 2t2e4 12137 . . . . . . . . . . . . . . . . . . 19 (2 · 2) = 4
314313, 250oveq12i 7287 . . . . . . . . . . . . . . . . . 18 ((2 · 2) + (0 + 1)) = (4 + 1)
315 4p1e5 12119 . . . . . . . . . . . . . . . . . 18 (4 + 1) = 5
316314, 315eqtri 2766 . . . . . . . . . . . . . . . . 17 ((2 · 2) + (0 + 1)) = 5
317 5t2e10 12537 . . . . . . . . . . . . . . . . . 18 (5 · 2) = 10
31893, 237, 250, 317decsuc 12468 . . . . . . . . . . . . . . . . 17 ((5 · 2) + 1) = 11
319233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318decmac 12489 . . . . . . . . . . . . . . . 16 ((25 · 2) + 1) = 51
320233, 310, 231, 311, 233, 93, 319, 255decmul1c 12502 . . . . . . . . . . . . . . 15 (256 · 2) = 512
321320a1i 11 . . . . . . . . . . . . . 14 (𝜑 → (256 · 2) = 512)
322309, 321eqtrd 2778 . . . . . . . . . . . . 13 (𝜑 → ((2↑8) · (2↑1)) = 512)
323303, 322eqtrd 2778 . . . . . . . . . . . 12 (𝜑 → (2↑9) = 512)
324323oveq1d 7290 . . . . . . . . . . 11 (𝜑 → ((2↑9) − 1) = (512 − 1))
325 1p1e2 12098 . . . . . . . . . . . . . 14 (1 + 1) = 2
326 eqid 2738 . . . . . . . . . . . . . 14 511 = 511
327272, 93, 325, 326decsuc 12468 . . . . . . . . . . . . 13 (511 + 1) = 512
328272, 233deccl 12452 . . . . . . . . . . . . . . 15 512 ∈ ℕ0
329328nn0cni 12245 . . . . . . . . . . . . . 14 512 ∈ ℂ
330272, 93deccl 12452 . . . . . . . . . . . . . . 15 511 ∈ ℕ0
331330nn0cni 12245 . . . . . . . . . . . . . 14 511 ∈ ℂ
332329, 242, 331subadd2i 11309 . . . . . . . . . . . . 13 ((512 − 1) = 511 ↔ (511 + 1) = 512)
333327, 332mpbir 230 . . . . . . . . . . . 12 (512 − 1) = 511
334333a1i 11 . . . . . . . . . . 11 (𝜑 → (512 − 1) = 511)
335324, 334eqtr2d 2779 . . . . . . . . . 10 (𝜑511 = ((2↑9) − 1))
336279, 295, 3353brtr3d 5105 . . . . . . . . 9 (𝜑 → ((3↑3) · (((3↑1) − 1) · ((3↑2) − 1))) < ((2↑9) − 1))
337216ltm1d 11907 . . . . . . . . . 10 (𝜑 → ((2↑9) − 1) < (2↑9))
338215nn0zd 12424 . . . . . . . . . . . 12 (𝜑 → 9 ∈ ℤ)
33973, 338, 143, 35leexp2d 13969 . . . . . . . . . . 11 (𝜑 → (9 ≤ (⌈‘((2 logb 3)↑5)) ↔ (2↑9) ≤ (2↑(⌈‘((2 logb 3)↑5)))))
34087, 339mpbid 231 . . . . . . . . . 10 (𝜑 → (2↑9) ≤ (2↑(⌈‘((2 logb 3)↑5))))
341217, 216, 224, 337, 340ltletrd 11135 . . . . . . . . 9 (𝜑 → ((2↑9) − 1) < (2↑(⌈‘((2 logb 3)↑5))))
342213, 217, 224, 336, 341lttrd 11136 . . . . . . . 8 (𝜑 → ((3↑3) · (((3↑1) − 1) · ((3↑2) − 1))) < (2↑(⌈‘((2 logb 3)↑5))))
343204, 342eqbrtrd 5096 . . . . . . 7 (𝜑 → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) < (2↑(⌈‘((2 logb 3)↑5))))
344343adantr 481 . . . . . 6 ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((3↑𝑘) − 1)) < (2↑(⌈‘((2 logb 3)↑5))))
34530, 344eqbrtrd 5096 . . . . 5 ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((𝑁𝑘) − 1)) < (2↑(⌈‘((2 logb 3)↑5))))
346 simpr 485 . . . . . . 7 ((𝜑 ∧ 3 = 𝑁) → 3 = 𝑁)
347 oveq2 7283 . . . . . . . . . . . . 13 (3 = 𝑁 → (2 logb 3) = (2 logb 𝑁))
348347adantl 482 . . . . . . . . . . . 12 ((𝜑 ∧ 3 = 𝑁) → (2 logb 3) = (2 logb 𝑁))
349348oveq1d 7290 . . . . . . . . . . 11 ((𝜑 ∧ 3 = 𝑁) → ((2 logb 3)↑5) = ((2 logb 𝑁)↑5))
350349fveq2d 6778 . . . . . . . . . 10 ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb 3)↑5)) = (⌈‘((2 logb 𝑁)↑5)))
3518a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ 3 = 𝑁) → 𝐵 = (⌈‘((2 logb 𝑁)↑5)))
352351eqcomd 2744 . . . . . . . . . 10 ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb 𝑁)↑5)) = 𝐵)
353350, 352eqtrd 2778 . . . . . . . . 9 ((𝜑 ∧ 3 = 𝑁) → (⌈‘((2 logb 3)↑5)) = 𝐵)
354353oveq2d 7291 . . . . . . . 8 ((𝜑 ∧ 3 = 𝑁) → (2 logb (⌈‘((2 logb 3)↑5))) = (2 logb 𝐵))
355354fveq2d 6778 . . . . . . 7 ((𝜑 ∧ 3 = 𝑁) → (⌊‘(2 logb (⌈‘((2 logb 3)↑5)))) = (⌊‘(2 logb 𝐵)))
356346, 355oveq12d 7293 . . . . . 6 ((𝜑 ∧ 3 = 𝑁) → (3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) = (𝑁↑(⌊‘(2 logb 𝐵))))
357346oveq2d 7291 . . . . . . . . . 10 ((𝜑 ∧ 3 = 𝑁) → (2 logb 3) = (2 logb 𝑁))
358357oveq1d 7290 . . . . . . . . 9 ((𝜑 ∧ 3 = 𝑁) → ((2 logb 3)↑2) = ((2 logb 𝑁)↑2))
359358fveq2d 6778 . . . . . . . 8 ((𝜑 ∧ 3 = 𝑁) → (⌊‘((2 logb 3)↑2)) = (⌊‘((2 logb 𝑁)↑2)))
360359oveq2d 7291 . . . . . . 7 ((𝜑 ∧ 3 = 𝑁) → (1...(⌊‘((2 logb 3)↑2))) = (1...(⌊‘((2 logb 𝑁)↑2))))
361360prodeq1d 15631 . . . . . 6 ((𝜑 ∧ 3 = 𝑁) → ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((𝑁𝑘) − 1) = ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
362356, 361oveq12d 7293 . . . . 5 ((𝜑 ∧ 3 = 𝑁) → ((3↑(⌊‘(2 logb (⌈‘((2 logb 3)↑5))))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 3)↑2)))((𝑁𝑘) − 1)) = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)))
363350oveq2d 7291 . . . . 5 ((𝜑 ∧ 3 = 𝑁) → (2↑(⌈‘((2 logb 3)↑5))) = (2↑(⌈‘((2 logb 𝑁)↑5))))
364345, 362, 3633brtr3d 5105 . . . 4 ((𝜑 ∧ 3 = 𝑁) → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) < (2↑(⌈‘((2 logb 𝑁)↑5))))
3657a1i 11 . . . . 5 ((𝜑 ∧ 3 = 𝑁) → 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)))
366365eqcomd 2744 . . . 4 ((𝜑 ∧ 3 = 𝑁) → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) = 𝐴)
3678oveq2i 7286 . . . . . 6 (2↑𝐵) = (2↑(⌈‘((2 logb 𝑁)↑5)))
368367a1i 11 . . . . 5 ((𝜑 ∧ 3 = 𝑁) → (2↑𝐵) = (2↑(⌈‘((2 logb 𝑁)↑5))))
369368eqcomd 2744 . . . 4 ((𝜑 ∧ 3 = 𝑁) → (2↑(⌈‘((2 logb 𝑁)↑5))) = (2↑𝐵))
370364, 366, 3693brtr3d 5105 . . 3 ((𝜑 ∧ 3 = 𝑁) → 𝐴 < (2↑𝐵))
371370ex 413 . 2 (𝜑 → (3 = 𝑁𝐴 < (2↑𝐵)))
372 eluzle 12595 . . . 4 (𝑁 ∈ (ℤ‘3) → 3 ≤ 𝑁)
3733, 372syl 17 . . 3 (𝜑 → 3 ≤ 𝑁)
37414zred 12426 . . . 4 (𝜑𝑁 ∈ ℝ)
37555, 374leloed 11118 . . 3 (𝜑 → (3 ≤ 𝑁 ↔ (3 < 𝑁 ∨ 3 = 𝑁)))
376373, 375mpbid 231 . 2 (𝜑 → (3 < 𝑁 ∨ 3 = 𝑁))
37723, 371, 376mpjaod 857 1 (𝜑𝐴 < (2↑𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1539  wcel 2106   class class class wbr 5074  cfv 6433  (class class class)co 7275  cc 10869  cr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009  cle 11010  cmin 11205  cn 11973  2c2 12028  3c3 12029  4c4 12030  5c5 12031  6c6 12032  7c7 12033  8c8 12034  9c9 12035  0cn0 12233  cz 12319  cdc 12437  cuz 12582  +crp 12730  ...cfz 13239  cfl 13510  cceil 13511  cexp 13782  cprod 15615   logb clogb 25914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949  ax-addf 10950  ax-mulf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-2o 8298  df-er 8498  df-map 8617  df-pm 8618  df-ixp 8686  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-fi 9170  df-sup 9201  df-inf 9202  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-5 12039  df-6 12040  df-7 12041  df-8 12042  df-9 12043  df-n0 12234  df-z 12320  df-dec 12438  df-uz 12583  df-q 12689  df-rp 12731  df-xneg 12848  df-xadd 12849  df-xmul 12850  df-ioo 13083  df-ioc 13084  df-ico 13085  df-icc 13086  df-fz 13240  df-fzo 13383  df-fl 13512  df-ceil 13513  df-mod 13590  df-seq 13722  df-exp 13783  df-fac 13988  df-bc 14017  df-hash 14045  df-shft 14778  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-limsup 15180  df-clim 15197  df-rlim 15198  df-sum 15398  df-prod 15616  df-ef 15777  df-e 15778  df-sin 15779  df-cos 15780  df-pi 15782  df-struct 16848  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-mulr 16976  df-starv 16977  df-sca 16978  df-vsca 16979  df-ip 16980  df-tset 16981  df-ple 16982  df-ds 16984  df-unif 16985  df-hom 16986  df-cco 16987  df-rest 17133  df-topn 17134  df-0g 17152  df-gsum 17153  df-topgen 17154  df-pt 17155  df-prds 17158  df-xrs 17213  df-qtop 17218  df-imas 17219  df-xps 17221  df-mre 17295  df-mrc 17296  df-acs 17298  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-psmet 20589  df-xmet 20590  df-met 20591  df-bl 20592  df-mopn 20593  df-fbas 20594  df-fg 20595  df-cnfld 20598  df-top 22043  df-topon 22060  df-topsp 22082  df-bases 22096  df-cld 22170  df-ntr 22171  df-cls 22172  df-nei 22249  df-lp 22287  df-perf 22288  df-cn 22378  df-cnp 22379  df-haus 22466  df-cmp 22538  df-tx 22713  df-hmeo 22906  df-fil 22997  df-fm 23089  df-flim 23090  df-flf 23091  df-xms 23473  df-ms 23474  df-tms 23475  df-cncf 24041  df-limc 25030  df-dv 25031  df-log 25712  df-cxp 25713  df-logb 25915
This theorem is referenced by:  aks4d1p3  40086
  Copyright terms: Public domain W3C validator