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 41248
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 12296 . . . . . 6 3 โˆˆ โ„•
21a1i 11 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„•)
3 aks4d1p1.1 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
43adantr 480 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
5 eluznn 12907 . . . . 5 ((3 โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3)) โ†’ ๐‘ โˆˆ โ„•)
62, 4, 5syl2anc 583 . . . 4 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ โ„•)
7 aks4d1p1.2 . . . 4 ๐ด = ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1))
8 aks4d1p1.3 . . . 4 ๐ต = (โŒˆโ€˜((2 logb ๐‘)โ†‘5))
9 3p1e4 12362 . . . . 5 (3 + 1) = 4
10 simpr 484 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 < ๐‘)
11 3z 12600 . . . . . . . 8 3 โˆˆ โ„ค
1211a1i 11 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„ค)
13 eluzelz 12837 . . . . . . . . 9 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ ๐‘ โˆˆ โ„ค)
143, 13syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
1514adantr 480 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ โ„ค)
1612, 15zltp1led 41152 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 < ๐‘ โ†” (3 + 1) โ‰ค ๐‘))
1710, 16mpbid 231 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 + 1) โ‰ค ๐‘)
189, 17eqbrtrrid 5185 . . . 4 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 4 โ‰ค ๐‘)
19 eqid 2731 . . . 4 (2 logb (((2 logb ๐‘)โ†‘5) + 1)) = (2 logb (((2 logb ๐‘)โ†‘5) + 1))
20 eqid 2731 . . . 4 ((2 logb ๐‘)โ†‘2) = ((2 logb ๐‘)โ†‘2)
21 eqid 2731 . . . 4 ((2 logb ๐‘)โ†‘4) = ((2 logb ๐‘)โ†‘4)
226, 7, 8, 18, 19, 20, 21aks4d1p1p5 41247 . . 3 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
2322ex 412 . 2 (๐œ‘ โ†’ (3 < ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
24 simp2 1136 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ 3 = ๐‘)
2524eqcomd 2737 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ๐‘ = 3)
2625oveq1d 7427 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ (๐‘โ†‘๐‘˜) = (3โ†‘๐‘˜))
2726oveq1d 7427 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
28273expa 1117 . . . . . . . 8 (((๐œ‘ โˆง 3 = ๐‘) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
2928prodeq2dv 15872 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1))
3029oveq2d 7428 . . . . . 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 12984 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
3231a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โˆˆ โ„+)
33 1red 11220 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 โˆˆ โ„)
34 1lt2 12388 . . . . . . . . . . . . . . . . . . 19 1 < 2
3534a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 < 2)
3633, 35ltned 11355 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โ‰  2)
3736necomd 2995 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โ‰  1)
3811a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 3 โˆˆ โ„ค)
3932, 37, 38relogbexpd 41146 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = 3)
4039eqcomd 2737 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 3 = (2 logb (2โ†‘3)))
41 cu2 14169 . . . . . . . . . . . . . . . 16 (2โ†‘3) = 8
4241a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘3) = 8)
4342oveq2d 7428 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = (2 logb 8))
4440, 43eqtrd 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 3 = (2 logb 8))
45 2z 12599 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
4645a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
4746zred 12671 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„)
4847leidd 11785 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค 2)
49 8re 12313 . . . . . . . . . . . . . . 15 8 โˆˆ โ„
5049a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 8 โˆˆ โ„)
51 8pos 12329 . . . . . . . . . . . . . . 15 0 < 8
5251a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 8)
5332rpgt0d 13024 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 2)
54 3re 12297 . . . . . . . . . . . . . . . . . . 19 3 โˆˆ โ„
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 3 โˆˆ โ„)
561nngt0i 12256 . . . . . . . . . . . . . . . . . . 19 0 < 3
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 3)
5847, 53, 55, 57, 37relogbcld 41145 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
59 5nn0 12497 . . . . . . . . . . . . . . . . . 18 5 โˆˆ โ„•0
6059a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 5 โˆˆ โ„•0)
6158, 60reexpcld 14133 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
62 ceilcl 13812 . . . . . . . . . . . . . . . 16 (((2 logb 3)โ†‘5) โˆˆ โ„ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6463zred 12671 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
65 0red 11222 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 0 โˆˆ โ„)
66 9re 12316 . . . . . . . . . . . . . . . . 17 9 โˆˆ โ„
6766a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โˆˆ โ„)
6850lep1d 12150 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 8 โ‰ค (8 + 1))
69 8p1e9 12367 . . . . . . . . . . . . . . . . . 18 (8 + 1) = 9
7069a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (8 + 1) = 9)
7168, 70breqtrd 5175 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 8 โ‰ค 9)
72 2re 12291 . . . . . . . . . . . . . . . . . . . 20 2 โˆˆ โ„
7372a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 2 โˆˆ โ„)
74 2pos 12320 . . . . . . . . . . . . . . . . . . . 20 0 < 2
7574a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 2)
76 3pos 12322 . . . . . . . . . . . . . . . . . . . 20 0 < 3
7776a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 3)
7873, 75, 55, 77, 37relogbcld 41145 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
7978, 60reexpcld 14133 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
8079, 62syl 17 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
8180zred 12671 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
8255leidd 11785 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 3 โ‰ค 3)
8355, 823lexlogpow5ineq4 41228 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 9 < ((2 logb 3)โ†‘5))
8467, 79, 83ltled 11367 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 9 โ‰ค ((2 logb 3)โ†‘5))
85 ceilge 13815 . . . . . . . . . . . . . . . . . 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 11376 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8850, 67, 64, 71, 87letrd 11376 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8965, 50, 64, 52, 88ltletrd 11379 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
9046, 48, 50, 52, 64, 89, 88logblebd 41148 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb 8) โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9144, 90eqbrtrd 5171 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9279, 33readdcld 11248 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((2 logb 3)โ†‘5) + 1) โˆˆ โ„)
93 1nn0 12493 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„•0
94 6nn 12306 . . . . . . . . . . . . . . . . . . 19 6 โˆˆ โ„•
9593, 94decnncl 12702 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„•
9695a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 16 โˆˆ โ„•)
9796nnred 12232 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 16 โˆˆ โ„)
98 ceilm1lt 13818 . . . . . . . . . . . . . . . . . 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 11815 . . . . . . . . . . . . . . . . 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 41232 . . . . . . . . . . . . . . . . . . 19 ((2 logb 3)โ†‘5) โ‰ค 15
103102a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค 15)
104 5p1e6 12364 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 1) = 6
105 eqid 2731 . . . . . . . . . . . . . . . . . . . . . 22 15 = 15
10693, 59, 104, 105decsuc 12713 . . . . . . . . . . . . . . . . . . . . 21 (15 + 1) = 16
107106a1i 11 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (15 + 1) = 16)
10897recnd 11247 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 16 โˆˆ โ„‚)
109 1cnd 11214 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
110 5nn 12303 . . . . . . . . . . . . . . . . . . . . . . . 24 5 โˆˆ โ„•
11193, 110decnncl 12702 . . . . . . . . . . . . . . . . . . . . . . 23 15 โˆˆ โ„•
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ 15 โˆˆ โ„•)
113112nncnd 12233 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 15 โˆˆ โ„‚)
114108, 109, 113subadd2d 11595 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((16 โˆ’ 1) = 15 โ†” (15 + 1) = 16))
115107, 114mpbird 256 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (16 โˆ’ 1) = 15)
116115eqcomd 2737 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 15 = (16 โˆ’ 1))
117103, 116breqtrd 5175 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1))
118 leaddsub 11695 . . . . . . . . . . . . . . . . . 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 11379 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < 16)
122 eqid 2731 . . . . . . . . . . . . . . . . 17 16 = 16
123 2exp4 17023 . . . . . . . . . . . . . . . . 17 (2โ†‘4) = 16
124122, 123eqtr4i 2762 . . . . . . . . . . . . . . . 16 16 = (2โ†‘4)
125124a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 16 = (2โ†‘4))
126121, 125breqtrd 5175 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < (2โ†‘4))
12746uzidd 12843 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜2))
12864, 89elrpd 13018 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„+)
129 4z 12601 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„ค
130129a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 4 โˆˆ โ„ค)
13132, 130rpexpcld 14215 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘4) โˆˆ โ„+)
132 logblt 26522 . . . . . . . . . . . . . . 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 41146 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = 4)
1369eqcomi 2740 . . . . . . . . . . . . . . 15 4 = (3 + 1)
137136a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 = (3 + 1))
138135, 137eqtrd 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = (3 + 1))
139134, 138breqtrd 5175 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) < (3 + 1))
14091, 139jca 511 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) โˆง (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) < (3 + 1)))
14173, 75, 55, 57, 37relogbcld 41145 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
142141, 60reexpcld 14133 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
143142, 62syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
144143zred 12671 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
145 9pos 12330 . . . . . . . . . . . . . . 15 0 < 9
146145a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 9)
14765, 67, 144, 146, 87ltletrd 11379 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
14873, 75, 144, 147, 37relogbcld 41145 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
149 flbi 13786 . . . . . . . . . . . 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 583 . . . . . . . . . . 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 7428 . . . . . . . . 9 (๐œ‘ โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (3โ†‘3))
15378resqcld 14095 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
154 3lexlogpow2ineq2 41231 . . . . . . . . . . . . . . . . 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 494 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 < ((2 logb 3)โ†‘2))
15773, 153, 156ltled 11367 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค ((2 logb 3)โ†‘2))
158155simprd 495 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < 3)
159 df-3 12281 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
160159a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 3 = (2 + 1))
161158, 160breqtrd 5175 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < (2 + 1))
162157, 161jca 511 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 โ‰ค ((2 logb 3)โ†‘2) โˆง ((2 logb 3)โ†‘2) < (2 + 1)))
163141resqcld 14095 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
164 flbi 13786 . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . 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 7428 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...2))
168167prodeq1d 15870 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1))
169 1zzd 12598 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
170169, 46jca 511 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค))
171 1le2 12426 . . . . . . . . . . . . . . 15 1 โ‰ค 2
172171a1i 11 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 1 โ‰ค 2)
173 eluz 12841 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ (2 โˆˆ (โ„คโ‰ฅโ€˜1) โ†” 1 โ‰ค 2))
174172, 173mpbird 256 . . . . . . . . . . . . 13 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
175170, 174syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
176 3cn 12298 . . . . . . . . . . . . . . 15 3 โˆˆ โ„‚
177176a1i 11 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 3 โˆˆ โ„‚)
178 elfznn 13535 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (1...2) โ†’ ๐‘˜ โˆˆ โ„•)
179178adantl 481 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•)
180179nnnn0d 12537 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•0)
181177, 180expcld 14116 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ (3โ†‘๐‘˜) โˆˆ โ„‚)
182 1cnd 11214 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 1 โˆˆ โ„‚)
183181, 182subcld 11576 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ((3โ†‘๐‘˜) โˆ’ 1) โˆˆ โ„‚)
184 oveq2 7420 . . . . . . . . . . . . 13 (๐‘˜ = 2 โ†’ (3โ†‘๐‘˜) = (3โ†‘2))
185184oveq1d 7427 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘2) โˆ’ 1))
186175, 183, 185fprodm1 15916 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
187 2m1e1 12343 . . . . . . . . . . . . . . . 16 (2 โˆ’ 1) = 1
188187a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 โˆ’ 1) = 1)
189188oveq2d 7428 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1...(2 โˆ’ 1)) = (1...1))
190189prodeq1d 15870 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...1)((3โ†‘๐‘˜) โˆ’ 1))
19155recnd 11247 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
19293a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โˆˆ โ„•0)
193191, 192expcld 14116 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„‚)
194193, 109subcld 11576 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚)
195169, 194jca 511 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚))
196 oveq2 7420 . . . . . . . . . . . . . . . 16 (๐‘˜ = 1 โ†’ (3โ†‘๐‘˜) = (3โ†‘1))
197196oveq1d 7427 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
198197fprod1 15912 . . . . . . . . . . . . . 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 2771 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
201200oveq1d 7427 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
202186, 201eqtrd 2771 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
203168, 202eqtrd 2771 . . . . . . . . 9 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
204152, 203oveq12d 7430 . . . . . . . 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 12495 . . . . . . . . . . . 12 3 โˆˆ โ„•0
206205a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
20755, 206reexpcld 14133 . . . . . . . . . 10 (๐œ‘ โ†’ (3โ†‘3) โˆˆ โ„)
20855, 192reexpcld 14133 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„)
209208, 33resubcld 11647 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„)
21055resqcld 14095 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘2) โˆˆ โ„)
211210, 33resubcld 11647 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) โˆˆ โ„)
212209, 211remulcld 11249 . . . . . . . . . 10 (๐œ‘ โ†’ (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) โˆˆ โ„)
213207, 212remulcld 11249 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) โˆˆ โ„)
214 9nn0 12501 . . . . . . . . . . . 12 9 โˆˆ โ„•0
215214a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 9 โˆˆ โ„•0)
21673, 215reexpcld 14133 . . . . . . . . . 10 (๐œ‘ โ†’ (2โ†‘9) โˆˆ โ„)
217216, 33resubcld 11647 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) โˆˆ โ„)
218 elnnz 12573 . . . . . . . . . . . . 13 ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โ†” ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค โˆง 0 < (โŒˆโ€˜((2 logb 3)โ†‘5))))
219143, 147, 218sylanbrc 582 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„•)
220219orcd 870 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โˆจ (โŒˆโ€˜((2 logb 3)โ†‘5)) = 0))
221 elnn0 12479 . . . . . . . . . . . 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 14133 . . . . . . . . 9 (๐œ‘ โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
225 8cn 12314 . . . . . . . . . . . . . . 15 8 โˆˆ โ„‚
226 2cn 12292 . . . . . . . . . . . . . . 15 2 โˆˆ โ„‚
227 8t2e16 12797 . . . . . . . . . . . . . . 15 (8 ยท 2) = 16
228225, 226, 227mulcomli 11228 . . . . . . . . . . . . . 14 (2 ยท 8) = 16
229228a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท 8) = 16)
230229oveq2d 7428 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = (27 ยท 16))
231 6nn0 12498 . . . . . . . . . . . . . . 15 6 โˆˆ โ„•0
23293, 231deccl 12697 . . . . . . . . . . . . . 14 16 โˆˆ โ„•0
233 2nn0 12494 . . . . . . . . . . . . . 14 2 โˆˆ โ„•0
234 7nn0 12499 . . . . . . . . . . . . . 14 7 โˆˆ โ„•0
235 eqid 2731 . . . . . . . . . . . . . 14 27 = 27
23693, 93deccl 12697 . . . . . . . . . . . . . 14 11 โˆˆ โ„•0
237 0nn0 12492 . . . . . . . . . . . . . . 15 0 โˆˆ โ„•0
238233dec0h 12704 . . . . . . . . . . . . . . 15 2 = 02
239 eqid 2731 . . . . . . . . . . . . . . 15 11 = 11
240232nn0cni 12489 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„‚
241240mul02i 11408 . . . . . . . . . . . . . . . . 17 (0 ยท 16) = 0
242 ax-1cn 11171 . . . . . . . . . . . . . . . . . 18 1 โˆˆ โ„‚
243176, 242, 9addcomli 11411 . . . . . . . . . . . . . . . . 17 (1 + 3) = 4
244241, 243oveq12i 7424 . . . . . . . . . . . . . . . 16 ((0 ยท 16) + (1 + 3)) = (0 + 4)
245 4cn 12302 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„‚
246245addlidi 11407 . . . . . . . . . . . . . . . 16 (0 + 4) = 4
247244, 246eqtri 2759 . . . . . . . . . . . . . . 15 ((0 ยท 16) + (1 + 3)) = 4
24893dec0h 12704 . . . . . . . . . . . . . . . 16 1 = 01
249 2t1e2 12380 . . . . . . . . . . . . . . . . . 18 (2 ยท 1) = 2
250 0p1e1 12339 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
251249, 250oveq12i 7424 . . . . . . . . . . . . . . . . 17 ((2 ยท 1) + (0 + 1)) = (2 + 1)
252 2p1e3 12359 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
253251, 252eqtri 2759 . . . . . . . . . . . . . . . 16 ((2 ยท 1) + (0 + 1)) = 3
254 6cn 12308 . . . . . . . . . . . . . . . . . 18 6 โˆˆ โ„‚
255 6t2e12 12786 . . . . . . . . . . . . . . . . . 18 (6 ยท 2) = 12
256254, 226, 255mulcomli 11228 . . . . . . . . . . . . . . . . 17 (2 ยท 6) = 12
25793, 233, 252, 256decsuc 12713 . . . . . . . . . . . . . . . 16 ((2 ยท 6) + 1) = 13
25893, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257decma2c 12735 . . . . . . . . . . . . . . 15 ((2 ยท 16) + 1) = 33
259237, 233, 93, 93, 238, 239, 232, 205, 205, 247, 258decmac 12734 . . . . . . . . . . . . . 14 ((2 ยท 16) + 11) = 43
260 4nn0 12496 . . . . . . . . . . . . . . 15 4 โˆˆ โ„•0
261 7cn 12311 . . . . . . . . . . . . . . . . . 18 7 โˆˆ โ„‚
262261mulridi 11223 . . . . . . . . . . . . . . . . 17 (7 ยท 1) = 7
263262oveq1i 7422 . . . . . . . . . . . . . . . 16 ((7 ยท 1) + 4) = (7 + 4)
264 7p4e11 12758 . . . . . . . . . . . . . . . 16 (7 + 4) = 11
265263, 264eqtri 2759 . . . . . . . . . . . . . . 15 ((7 ยท 1) + 4) = 11
266 7t6e42 12795 . . . . . . . . . . . . . . 15 (7 ยท 6) = 42
267234, 93, 231, 122, 233, 260, 265, 266decmul2c 12748 . . . . . . . . . . . . . 14 (7 ยท 16) = 112
268232, 233, 234, 235, 233, 236, 259, 267decmul1c 12747 . . . . . . . . . . . . 13 (27 ยท 16) = 432
269268a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท 16) = 432)
270230, 269eqtrd 2771 . . . . . . . . . . 11 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = 432)
271260, 205deccl 12697 . . . . . . . . . . . . 13 43 โˆˆ โ„•0
27259, 93deccl 12697 . . . . . . . . . . . . 13 51 โˆˆ โ„•0
273 2lt10 12820 . . . . . . . . . . . . 13 2 < 10
274 3lt10 12819 . . . . . . . . . . . . . 14 3 < 10
275 4lt5 12394 . . . . . . . . . . . . . 14 4 < 5
276260, 59, 205, 93, 274, 275decltc 12711 . . . . . . . . . . . . 13 43 < 51
277271, 272, 233, 93, 273, 276decltc 12711 . . . . . . . . . . . 12 432 < 511
278277a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 432 < 511)
279270, 278eqbrtrd 5171 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) < 511)
280 3exp3 17030 . . . . . . . . . . . . 13 (3โ†‘3) = 27
281280a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘3) = 27)
282281eqcomd 2737 . . . . . . . . . . 11 (๐œ‘ โ†’ 27 = (3โ†‘3))
283191exp1d 14111 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘1) = 3)
284283oveq1d 7427 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) = (3 โˆ’ 1))
285 3m1e2 12345 . . . . . . . . . . . . . 14 (3 โˆ’ 1) = 2
286285a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 โˆ’ 1) = 2)
287284, 286eqtr2d 2772 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 = ((3โ†‘1) โˆ’ 1))
288 sq3 14167 . . . . . . . . . . . . . . 15 (3โ†‘2) = 9
289288a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘2) = 9)
290289oveq1d 7427 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) = (9 โˆ’ 1))
291 9m1e8 12351 . . . . . . . . . . . . . 14 (9 โˆ’ 1) = 8
292291a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (9 โˆ’ 1) = 8)
293290, 292eqtr2d 2772 . . . . . . . . . . . 12 (๐œ‘ โ†’ 8 = ((3โ†‘2) โˆ’ 1))
294287, 293oveq12d 7430 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท 8) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
295282, 294oveq12d 7430 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))))
296 df-9 12287 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
297296a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 9 = (8 + 1))
298297oveq2d 7428 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘9) = (2โ†‘(8 + 1)))
299287, 194eqeltrd 2832 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
300 8nn0 12500 . . . . . . . . . . . . . . . 16 8 โˆˆ โ„•0
301300a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โˆˆ โ„•0)
302299, 192, 301expaddd 14118 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘(8 + 1)) = ((2โ†‘8) ยท (2โ†‘1)))
303298, 302eqtrd 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2โ†‘9) = ((2โ†‘8) ยท (2โ†‘1)))
304 2exp8 17027 . . . . . . . . . . . . . . . . 17 (2โ†‘8) = 256
305304a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘8) = 256)
306305oveq1d 7427 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท (2โ†‘1)))
307299exp1d 14111 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘1) = 2)
308307oveq2d 7428 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (256 ยท (2โ†‘1)) = (256 ยท 2))
309306, 308eqtrd 2771 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท 2))
310233, 59deccl 12697 . . . . . . . . . . . . . . . 16 25 โˆˆ โ„•0
311 eqid 2731 . . . . . . . . . . . . . . . 16 256 = 256
312 eqid 2731 . . . . . . . . . . . . . . . . 17 25 = 25
313 2t2e4 12381 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
314313, 250oveq12i 7424 . . . . . . . . . . . . . . . . . 18 ((2 ยท 2) + (0 + 1)) = (4 + 1)
315 4p1e5 12363 . . . . . . . . . . . . . . . . . 18 (4 + 1) = 5
316314, 315eqtri 2759 . . . . . . . . . . . . . . . . 17 ((2 ยท 2) + (0 + 1)) = 5
317 5t2e10 12782 . . . . . . . . . . . . . . . . . 18 (5 ยท 2) = 10
31893, 237, 250, 317decsuc 12713 . . . . . . . . . . . . . . . . 17 ((5 ยท 2) + 1) = 11
319233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318decmac 12734 . . . . . . . . . . . . . . . 16 ((25 ยท 2) + 1) = 51
320233, 310, 231, 311, 233, 93, 319, 255decmul1c 12747 . . . . . . . . . . . . . . 15 (256 ยท 2) = 512
321320a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (256 ยท 2) = 512)
322309, 321eqtrd 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = 512)
323303, 322eqtrd 2771 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2โ†‘9) = 512)
324323oveq1d 7427 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) = (512 โˆ’ 1))
325 1p1e2 12342 . . . . . . . . . . . . . 14 (1 + 1) = 2
326 eqid 2731 . . . . . . . . . . . . . 14 511 = 511
327272, 93, 325, 326decsuc 12713 . . . . . . . . . . . . 13 (511 + 1) = 512
328272, 233deccl 12697 . . . . . . . . . . . . . . 15 512 โˆˆ โ„•0
329328nn0cni 12489 . . . . . . . . . . . . . 14 512 โˆˆ โ„‚
330272, 93deccl 12697 . . . . . . . . . . . . . . 15 511 โˆˆ โ„•0
331330nn0cni 12489 . . . . . . . . . . . . . 14 511 โˆˆ โ„‚
332329, 242, 331subadd2i 11553 . . . . . . . . . . . . 13 ((512 โˆ’ 1) = 511 โ†” (511 + 1) = 512)
333327, 332mpbir 230 . . . . . . . . . . . 12 (512 โˆ’ 1) = 511
334333a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (512 โˆ’ 1) = 511)
335324, 334eqtr2d 2772 . . . . . . . . . 10 (๐œ‘ โ†’ 511 = ((2โ†‘9) โˆ’ 1))
336279, 295, 3353brtr3d 5180 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < ((2โ†‘9) โˆ’ 1))
337216ltm1d 12151 . . . . . . . . . 10 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘9))
338215nn0zd 12589 . . . . . . . . . . . 12 (๐œ‘ โ†’ 9 โˆˆ โ„ค)
33973, 338, 143, 35leexp2d 14220 . . . . . . . . . . 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 11379 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
342213, 217, 224, 336, 341lttrd 11380 . . . . . . . 8 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
343204, 342eqbrtrd 5171 . . . . . . 7 (๐œ‘ โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
344343adantr 480 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
34530, 344eqbrtrd 5171 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
346 simpr 484 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ 3 = ๐‘)
347 oveq2 7420 . . . . . . . . . . . . 13 (3 = ๐‘ โ†’ (2 logb 3) = (2 logb ๐‘))
348347adantl 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
349348oveq1d 7427 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘5) = ((2 logb ๐‘)โ†‘5))
350349fveq2d 6896 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
3518a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ต = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
352351eqcomd 2737 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb ๐‘)โ†‘5)) = ๐ต)
353350, 352eqtrd 2771 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = ๐ต)
354353oveq2d 7428 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) = (2 logb ๐ต))
355354fveq2d 6896 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5)))) = (โŒŠโ€˜(2 logb ๐ต)))
356346, 355oveq12d 7430 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))))
357346oveq2d 7428 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
358357oveq1d 7427 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘2) = ((2 logb ๐‘)โ†‘2))
359358fveq2d 6896 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜((2 logb 3)โ†‘2)) = (โŒŠโ€˜((2 logb ๐‘)โ†‘2)))
360359oveq2d 7428 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2))))
361360prodeq1d 15870 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1))
362356, 361oveq12d 7430 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)))
363350oveq2d 7428 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
364345, 362, 3633brtr3d 5180 . . . 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 2737 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ๐ด)
3678oveq2i 7423 . . . . . 6 (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
368367a1i 11 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
369368eqcomd 2737 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))) = (2โ†‘๐ต))
370364, 366, 3693brtr3d 5180 . . 3 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
371370ex 412 . 2 (๐œ‘ โ†’ (3 = ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
372 eluzle 12840 . . . 4 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ 3 โ‰ค ๐‘)
3733, 372syl 17 . . 3 (๐œ‘ โ†’ 3 โ‰ค ๐‘)
37414zred 12671 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
37555, 374leloed 11362 . . 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 395   โˆจ wo 844   โˆง w3a 1086   = wceq 1540   โˆˆ wcel 2105   class class class wbr 5149  โ€˜cfv 6544  (class class class)co 7412  โ„‚cc 11111  โ„cr 11112  0cc0 11113  1c1 11114   + caddc 11116   ยท cmul 11118   < clt 11253   โ‰ค cle 11254   โˆ’ cmin 11449  โ„•cn 12217  2c2 12272  3c3 12273  4c4 12274  5c5 12275  6c6 12276  7c7 12277  8c8 12278  9c9 12279  โ„•0cn0 12477  โ„คcz 12563  cdc 12682  โ„คโ‰ฅcuz 12827  โ„+crp 12979  ...cfz 13489  โŒŠcfl 13760  โŒˆcceil 13761  โ†‘cexp 14032  โˆcprod 15854   logb clogb 26502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-inf2 9639  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191  ax-addf 11192  ax-mulf 11193
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7673  df-om 7859  df-1st 7978  df-2nd 7979  df-supp 8150  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-2o 8470  df-er 8706  df-map 8825  df-pm 8826  df-ixp 8895  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-fsupp 9365  df-fi 9409  df-sup 9440  df-inf 9441  df-oi 9508  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-z 12564  df-dec 12683  df-uz 12828  df-q 12938  df-rp 12980  df-xneg 13097  df-xadd 13098  df-xmul 13099  df-ioo 13333  df-ioc 13334  df-ico 13335  df-icc 13336  df-fz 13490  df-fzo 13633  df-fl 13762  df-ceil 13763  df-mod 13840  df-seq 13972  df-exp 14033  df-fac 14239  df-bc 14268  df-hash 14296  df-shft 15019  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-limsup 15420  df-clim 15437  df-rlim 15438  df-sum 15638  df-prod 15855  df-ef 16016  df-e 16017  df-sin 16018  df-cos 16019  df-pi 16021  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18566  df-sgrp 18645  df-mnd 18661  df-submnd 18707  df-mulg 18988  df-cntz 19223  df-cmn 19692  df-psmet 21137  df-xmet 21138  df-met 21139  df-bl 21140  df-mopn 21141  df-fbas 21142  df-fg 21143  df-cnfld 21146  df-top 22617  df-topon 22634  df-topsp 22656  df-bases 22670  df-cld 22744  df-ntr 22745  df-cls 22746  df-nei 22823  df-lp 22861  df-perf 22862  df-cn 22952  df-cnp 22953  df-haus 23040  df-cmp 23112  df-tx 23287  df-hmeo 23480  df-fil 23571  df-fm 23663  df-flim 23664  df-flf 23665  df-xms 24047  df-ms 24048  df-tms 24049  df-cncf 24619  df-limc 25616  df-dv 25617  df-log 26298  df-cxp 26299  df-logb 26503
This theorem is referenced by:  aks4d1p3  41250
  Copyright terms: Public domain W3C validator