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 41027
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 12293 . . . . . 6 3 โˆˆ โ„•
21a1i 11 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„•)
3 aks4d1p1.1 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
43adantr 481 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
5 eluznn 12904 . . . . 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 12359 . . . . 5 (3 + 1) = 4
10 simpr 485 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 < ๐‘)
11 3z 12597 . . . . . . . 8 3 โˆˆ โ„ค
1211a1i 11 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„ค)
13 eluzelz 12834 . . . . . . . . 9 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ ๐‘ โˆˆ โ„ค)
143, 13syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
1514adantr 481 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ โ„ค)
1612, 15zltp1led 40931 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 < ๐‘ โ†” (3 + 1) โ‰ค ๐‘))
1710, 16mpbid 231 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 + 1) โ‰ค ๐‘)
189, 17eqbrtrrid 5184 . . . 4 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 4 โ‰ค ๐‘)
19 eqid 2732 . . . 4 (2 logb (((2 logb ๐‘)โ†‘5) + 1)) = (2 logb (((2 logb ๐‘)โ†‘5) + 1))
20 eqid 2732 . . . 4 ((2 logb ๐‘)โ†‘2) = ((2 logb ๐‘)โ†‘2)
21 eqid 2732 . . . 4 ((2 logb ๐‘)โ†‘4) = ((2 logb ๐‘)โ†‘4)
226, 7, 8, 18, 19, 20, 21aks4d1p1p5 41026 . . 3 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
2322ex 413 . 2 (๐œ‘ โ†’ (3 < ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
24 simp2 1137 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ 3 = ๐‘)
2524eqcomd 2738 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ๐‘ = 3)
2625oveq1d 7426 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ (๐‘โ†‘๐‘˜) = (3โ†‘๐‘˜))
2726oveq1d 7426 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
28273expa 1118 . . . . . . . 8 (((๐œ‘ โˆง 3 = ๐‘) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
2928prodeq2dv 15869 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1))
3029oveq2d 7427 . . . . . 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 12981 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
3231a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โˆˆ โ„+)
33 1red 11217 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 โˆˆ โ„)
34 1lt2 12385 . . . . . . . . . . . . . . . . . . 19 1 < 2
3534a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 < 2)
3633, 35ltned 11352 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โ‰  2)
3736necomd 2996 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โ‰  1)
3811a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 3 โˆˆ โ„ค)
3932, 37, 38relogbexpd 40925 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = 3)
4039eqcomd 2738 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 3 = (2 logb (2โ†‘3)))
41 cu2 14166 . . . . . . . . . . . . . . . 16 (2โ†‘3) = 8
4241a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘3) = 8)
4342oveq2d 7427 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = (2 logb 8))
4440, 43eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 3 = (2 logb 8))
45 2z 12596 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
4645a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
4746zred 12668 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„)
4847leidd 11782 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค 2)
49 8re 12310 . . . . . . . . . . . . . . 15 8 โˆˆ โ„
5049a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 8 โˆˆ โ„)
51 8pos 12326 . . . . . . . . . . . . . . 15 0 < 8
5251a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 8)
5332rpgt0d 13021 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 2)
54 3re 12294 . . . . . . . . . . . . . . . . . . 19 3 โˆˆ โ„
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 3 โˆˆ โ„)
561nngt0i 12253 . . . . . . . . . . . . . . . . . . 19 0 < 3
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 3)
5847, 53, 55, 57, 37relogbcld 40924 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
59 5nn0 12494 . . . . . . . . . . . . . . . . . 18 5 โˆˆ โ„•0
6059a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 5 โˆˆ โ„•0)
6158, 60reexpcld 14130 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
62 ceilcl 13809 . . . . . . . . . . . . . . . 16 (((2 logb 3)โ†‘5) โˆˆ โ„ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6463zred 12668 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
65 0red 11219 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 0 โˆˆ โ„)
66 9re 12313 . . . . . . . . . . . . . . . . 17 9 โˆˆ โ„
6766a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โˆˆ โ„)
6850lep1d 12147 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 8 โ‰ค (8 + 1))
69 8p1e9 12364 . . . . . . . . . . . . . . . . . 18 (8 + 1) = 9
7069a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (8 + 1) = 9)
7168, 70breqtrd 5174 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 8 โ‰ค 9)
72 2re 12288 . . . . . . . . . . . . . . . . . . . 20 2 โˆˆ โ„
7372a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 2 โˆˆ โ„)
74 2pos 12317 . . . . . . . . . . . . . . . . . . . 20 0 < 2
7574a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 2)
76 3pos 12319 . . . . . . . . . . . . . . . . . . . 20 0 < 3
7776a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 3)
7873, 75, 55, 77, 37relogbcld 40924 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
7978, 60reexpcld 14130 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
8079, 62syl 17 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
8180zred 12668 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
8255leidd 11782 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 3 โ‰ค 3)
8355, 823lexlogpow5ineq4 41007 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 9 < ((2 logb 3)โ†‘5))
8467, 79, 83ltled 11364 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 9 โ‰ค ((2 logb 3)โ†‘5))
85 ceilge 13812 . . . . . . . . . . . . . . . . . 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 11373 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8850, 67, 64, 71, 87letrd 11373 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8965, 50, 64, 52, 88ltletrd 11376 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
9046, 48, 50, 52, 64, 89, 88logblebd 40927 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb 8) โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9144, 90eqbrtrd 5170 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9279, 33readdcld 11245 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((2 logb 3)โ†‘5) + 1) โˆˆ โ„)
93 1nn0 12490 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„•0
94 6nn 12303 . . . . . . . . . . . . . . . . . . 19 6 โˆˆ โ„•
9593, 94decnncl 12699 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„•
9695a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 16 โˆˆ โ„•)
9796nnred 12229 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 16 โˆˆ โ„)
98 ceilm1lt 13815 . . . . . . . . . . . . . . . . . 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 11812 . . . . . . . . . . . . . . . . 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 41011 . . . . . . . . . . . . . . . . . . 19 ((2 logb 3)โ†‘5) โ‰ค 15
103102a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค 15)
104 5p1e6 12361 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 1) = 6
105 eqid 2732 . . . . . . . . . . . . . . . . . . . . . 22 15 = 15
10693, 59, 104, 105decsuc 12710 . . . . . . . . . . . . . . . . . . . . 21 (15 + 1) = 16
107106a1i 11 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (15 + 1) = 16)
10897recnd 11244 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 16 โˆˆ โ„‚)
109 1cnd 11211 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
110 5nn 12300 . . . . . . . . . . . . . . . . . . . . . . . 24 5 โˆˆ โ„•
11193, 110decnncl 12699 . . . . . . . . . . . . . . . . . . . . . . 23 15 โˆˆ โ„•
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ 15 โˆˆ โ„•)
113112nncnd 12230 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 15 โˆˆ โ„‚)
114108, 109, 113subadd2d 11592 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((16 โˆ’ 1) = 15 โ†” (15 + 1) = 16))
115107, 114mpbird 256 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (16 โˆ’ 1) = 15)
116115eqcomd 2738 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 15 = (16 โˆ’ 1))
117103, 116breqtrd 5174 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1))
118 leaddsub 11692 . . . . . . . . . . . . . . . . . 18 ((((2 logb 3)โ†‘5) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง 16 โˆˆ โ„) โ†’ ((((2 logb 3)โ†‘5) + 1) โ‰ค 16 โ†” ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1)))
11979, 33, 97, 118syl3anc 1371 . . . . . . . . . . . . . . . . 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 11376 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < 16)
122 eqid 2732 . . . . . . . . . . . . . . . . 17 16 = 16
123 2exp4 17020 . . . . . . . . . . . . . . . . 17 (2โ†‘4) = 16
124122, 123eqtr4i 2763 . . . . . . . . . . . . . . . 16 16 = (2โ†‘4)
125124a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 16 = (2โ†‘4))
126121, 125breqtrd 5174 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < (2โ†‘4))
12746uzidd 12840 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜2))
12864, 89elrpd 13015 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„+)
129 4z 12598 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„ค
130129a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 4 โˆˆ โ„ค)
13132, 130rpexpcld 14212 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘4) โˆˆ โ„+)
132 logblt 26296 . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . 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 40925 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = 4)
1369eqcomi 2741 . . . . . . . . . . . . . . 15 4 = (3 + 1)
137136a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 = (3 + 1))
138135, 137eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = (3 + 1))
139134, 138breqtrd 5174 . . . . . . . . . . . 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 40924 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
142141, 60reexpcld 14130 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
143142, 62syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
144143zred 12668 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
145 9pos 12327 . . . . . . . . . . . . . . 15 0 < 9
146145a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 9)
14765, 67, 144, 146, 87ltletrd 11376 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
14873, 75, 144, 147, 37relogbcld 40924 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
149 flbi 13783 . . . . . . . . . . . 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 7427 . . . . . . . . 9 (๐œ‘ โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (3โ†‘3))
15378resqcld 14092 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
154 3lexlogpow2ineq2 41010 . . . . . . . . . . . . . . . . 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 11364 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค ((2 logb 3)โ†‘2))
158155simprd 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < 3)
159 df-3 12278 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
160159a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 3 = (2 + 1))
161158, 160breqtrd 5174 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < (2 + 1))
162157, 161jca 512 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 โ‰ค ((2 logb 3)โ†‘2) โˆง ((2 logb 3)โ†‘2) < (2 + 1)))
163141resqcld 14092 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
164 flbi 13783 . . . . . . . . . . . . . 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 7427 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...2))
168167prodeq1d 15867 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1))
169 1zzd 12595 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
170169, 46jca 512 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค))
171 1le2 12423 . . . . . . . . . . . . . . 15 1 โ‰ค 2
172171a1i 11 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 1 โ‰ค 2)
173 eluz 12838 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ (2 โˆˆ (โ„คโ‰ฅโ€˜1) โ†” 1 โ‰ค 2))
174172, 173mpbird 256 . . . . . . . . . . . . 13 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
175170, 174syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
176 3cn 12295 . . . . . . . . . . . . . . 15 3 โˆˆ โ„‚
177176a1i 11 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 3 โˆˆ โ„‚)
178 elfznn 13532 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (1...2) โ†’ ๐‘˜ โˆˆ โ„•)
179178adantl 482 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•)
180179nnnn0d 12534 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•0)
181177, 180expcld 14113 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ (3โ†‘๐‘˜) โˆˆ โ„‚)
182 1cnd 11211 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 1 โˆˆ โ„‚)
183181, 182subcld 11573 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ((3โ†‘๐‘˜) โˆ’ 1) โˆˆ โ„‚)
184 oveq2 7419 . . . . . . . . . . . . 13 (๐‘˜ = 2 โ†’ (3โ†‘๐‘˜) = (3โ†‘2))
185184oveq1d 7426 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘2) โˆ’ 1))
186175, 183, 185fprodm1 15913 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
187 2m1e1 12340 . . . . . . . . . . . . . . . 16 (2 โˆ’ 1) = 1
188187a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 โˆ’ 1) = 1)
189188oveq2d 7427 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1...(2 โˆ’ 1)) = (1...1))
190189prodeq1d 15867 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...1)((3โ†‘๐‘˜) โˆ’ 1))
19155recnd 11244 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
19293a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โˆˆ โ„•0)
193191, 192expcld 14113 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„‚)
194193, 109subcld 11573 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚)
195169, 194jca 512 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚))
196 oveq2 7419 . . . . . . . . . . . . . . . 16 (๐‘˜ = 1 โ†’ (3โ†‘๐‘˜) = (3โ†‘1))
197196oveq1d 7426 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
198197fprod1 15909 . . . . . . . . . . . . . 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 2772 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
201200oveq1d 7426 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
202186, 201eqtrd 2772 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
203168, 202eqtrd 2772 . . . . . . . . 9 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
204152, 203oveq12d 7429 . . . . . . . 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 12492 . . . . . . . . . . . 12 3 โˆˆ โ„•0
206205a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
20755, 206reexpcld 14130 . . . . . . . . . 10 (๐œ‘ โ†’ (3โ†‘3) โˆˆ โ„)
20855, 192reexpcld 14130 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„)
209208, 33resubcld 11644 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„)
21055resqcld 14092 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘2) โˆˆ โ„)
211210, 33resubcld 11644 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) โˆˆ โ„)
212209, 211remulcld 11246 . . . . . . . . . 10 (๐œ‘ โ†’ (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) โˆˆ โ„)
213207, 212remulcld 11246 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) โˆˆ โ„)
214 9nn0 12498 . . . . . . . . . . . 12 9 โˆˆ โ„•0
215214a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 9 โˆˆ โ„•0)
21673, 215reexpcld 14130 . . . . . . . . . 10 (๐œ‘ โ†’ (2โ†‘9) โˆˆ โ„)
217216, 33resubcld 11644 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) โˆˆ โ„)
218 elnnz 12570 . . . . . . . . . . . . 13 ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โ†” ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค โˆง 0 < (โŒˆโ€˜((2 logb 3)โ†‘5))))
219143, 147, 218sylanbrc 583 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„•)
220219orcd 871 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โˆจ (โŒˆโ€˜((2 logb 3)โ†‘5)) = 0))
221 elnn0 12476 . . . . . . . . . . . 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 14130 . . . . . . . . 9 (๐œ‘ โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
225 8cn 12311 . . . . . . . . . . . . . . 15 8 โˆˆ โ„‚
226 2cn 12289 . . . . . . . . . . . . . . 15 2 โˆˆ โ„‚
227 8t2e16 12794 . . . . . . . . . . . . . . 15 (8 ยท 2) = 16
228225, 226, 227mulcomli 11225 . . . . . . . . . . . . . 14 (2 ยท 8) = 16
229228a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท 8) = 16)
230229oveq2d 7427 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = (27 ยท 16))
231 6nn0 12495 . . . . . . . . . . . . . . 15 6 โˆˆ โ„•0
23293, 231deccl 12694 . . . . . . . . . . . . . 14 16 โˆˆ โ„•0
233 2nn0 12491 . . . . . . . . . . . . . 14 2 โˆˆ โ„•0
234 7nn0 12496 . . . . . . . . . . . . . 14 7 โˆˆ โ„•0
235 eqid 2732 . . . . . . . . . . . . . 14 27 = 27
23693, 93deccl 12694 . . . . . . . . . . . . . 14 11 โˆˆ โ„•0
237 0nn0 12489 . . . . . . . . . . . . . . 15 0 โˆˆ โ„•0
238233dec0h 12701 . . . . . . . . . . . . . . 15 2 = 02
239 eqid 2732 . . . . . . . . . . . . . . 15 11 = 11
240232nn0cni 12486 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„‚
241240mul02i 11405 . . . . . . . . . . . . . . . . 17 (0 ยท 16) = 0
242 ax-1cn 11170 . . . . . . . . . . . . . . . . . 18 1 โˆˆ โ„‚
243176, 242, 9addcomli 11408 . . . . . . . . . . . . . . . . 17 (1 + 3) = 4
244241, 243oveq12i 7423 . . . . . . . . . . . . . . . 16 ((0 ยท 16) + (1 + 3)) = (0 + 4)
245 4cn 12299 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„‚
246245addlidi 11404 . . . . . . . . . . . . . . . 16 (0 + 4) = 4
247244, 246eqtri 2760 . . . . . . . . . . . . . . 15 ((0 ยท 16) + (1 + 3)) = 4
24893dec0h 12701 . . . . . . . . . . . . . . . 16 1 = 01
249 2t1e2 12377 . . . . . . . . . . . . . . . . . 18 (2 ยท 1) = 2
250 0p1e1 12336 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
251249, 250oveq12i 7423 . . . . . . . . . . . . . . . . 17 ((2 ยท 1) + (0 + 1)) = (2 + 1)
252 2p1e3 12356 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
253251, 252eqtri 2760 . . . . . . . . . . . . . . . 16 ((2 ยท 1) + (0 + 1)) = 3
254 6cn 12305 . . . . . . . . . . . . . . . . . 18 6 โˆˆ โ„‚
255 6t2e12 12783 . . . . . . . . . . . . . . . . . 18 (6 ยท 2) = 12
256254, 226, 255mulcomli 11225 . . . . . . . . . . . . . . . . 17 (2 ยท 6) = 12
25793, 233, 252, 256decsuc 12710 . . . . . . . . . . . . . . . 16 ((2 ยท 6) + 1) = 13
25893, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257decma2c 12732 . . . . . . . . . . . . . . 15 ((2 ยท 16) + 1) = 33
259237, 233, 93, 93, 238, 239, 232, 205, 205, 247, 258decmac 12731 . . . . . . . . . . . . . 14 ((2 ยท 16) + 11) = 43
260 4nn0 12493 . . . . . . . . . . . . . . 15 4 โˆˆ โ„•0
261 7cn 12308 . . . . . . . . . . . . . . . . . 18 7 โˆˆ โ„‚
262261mulridi 11220 . . . . . . . . . . . . . . . . 17 (7 ยท 1) = 7
263262oveq1i 7421 . . . . . . . . . . . . . . . 16 ((7 ยท 1) + 4) = (7 + 4)
264 7p4e11 12755 . . . . . . . . . . . . . . . 16 (7 + 4) = 11
265263, 264eqtri 2760 . . . . . . . . . . . . . . 15 ((7 ยท 1) + 4) = 11
266 7t6e42 12792 . . . . . . . . . . . . . . 15 (7 ยท 6) = 42
267234, 93, 231, 122, 233, 260, 265, 266decmul2c 12745 . . . . . . . . . . . . . 14 (7 ยท 16) = 112
268232, 233, 234, 235, 233, 236, 259, 267decmul1c 12744 . . . . . . . . . . . . 13 (27 ยท 16) = 432
269268a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท 16) = 432)
270230, 269eqtrd 2772 . . . . . . . . . . 11 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = 432)
271260, 205deccl 12694 . . . . . . . . . . . . 13 43 โˆˆ โ„•0
27259, 93deccl 12694 . . . . . . . . . . . . 13 51 โˆˆ โ„•0
273 2lt10 12817 . . . . . . . . . . . . 13 2 < 10
274 3lt10 12816 . . . . . . . . . . . . . 14 3 < 10
275 4lt5 12391 . . . . . . . . . . . . . 14 4 < 5
276260, 59, 205, 93, 274, 275decltc 12708 . . . . . . . . . . . . 13 43 < 51
277271, 272, 233, 93, 273, 276decltc 12708 . . . . . . . . . . . 12 432 < 511
278277a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 432 < 511)
279270, 278eqbrtrd 5170 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) < 511)
280 3exp3 17027 . . . . . . . . . . . . 13 (3โ†‘3) = 27
281280a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘3) = 27)
282281eqcomd 2738 . . . . . . . . . . 11 (๐œ‘ โ†’ 27 = (3โ†‘3))
283191exp1d 14108 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘1) = 3)
284283oveq1d 7426 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) = (3 โˆ’ 1))
285 3m1e2 12342 . . . . . . . . . . . . . 14 (3 โˆ’ 1) = 2
286285a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 โˆ’ 1) = 2)
287284, 286eqtr2d 2773 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 = ((3โ†‘1) โˆ’ 1))
288 sq3 14164 . . . . . . . . . . . . . . 15 (3โ†‘2) = 9
289288a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘2) = 9)
290289oveq1d 7426 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) = (9 โˆ’ 1))
291 9m1e8 12348 . . . . . . . . . . . . . 14 (9 โˆ’ 1) = 8
292291a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (9 โˆ’ 1) = 8)
293290, 292eqtr2d 2773 . . . . . . . . . . . 12 (๐œ‘ โ†’ 8 = ((3โ†‘2) โˆ’ 1))
294287, 293oveq12d 7429 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท 8) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
295282, 294oveq12d 7429 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))))
296 df-9 12284 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
297296a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 9 = (8 + 1))
298297oveq2d 7427 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘9) = (2โ†‘(8 + 1)))
299287, 194eqeltrd 2833 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
300 8nn0 12497 . . . . . . . . . . . . . . . 16 8 โˆˆ โ„•0
301300a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โˆˆ โ„•0)
302299, 192, 301expaddd 14115 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘(8 + 1)) = ((2โ†‘8) ยท (2โ†‘1)))
303298, 302eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2โ†‘9) = ((2โ†‘8) ยท (2โ†‘1)))
304 2exp8 17024 . . . . . . . . . . . . . . . . 17 (2โ†‘8) = 256
305304a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘8) = 256)
306305oveq1d 7426 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท (2โ†‘1)))
307299exp1d 14108 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘1) = 2)
308307oveq2d 7427 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (256 ยท (2โ†‘1)) = (256 ยท 2))
309306, 308eqtrd 2772 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท 2))
310233, 59deccl 12694 . . . . . . . . . . . . . . . 16 25 โˆˆ โ„•0
311 eqid 2732 . . . . . . . . . . . . . . . 16 256 = 256
312 eqid 2732 . . . . . . . . . . . . . . . . 17 25 = 25
313 2t2e4 12378 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
314313, 250oveq12i 7423 . . . . . . . . . . . . . . . . . 18 ((2 ยท 2) + (0 + 1)) = (4 + 1)
315 4p1e5 12360 . . . . . . . . . . . . . . . . . 18 (4 + 1) = 5
316314, 315eqtri 2760 . . . . . . . . . . . . . . . . 17 ((2 ยท 2) + (0 + 1)) = 5
317 5t2e10 12779 . . . . . . . . . . . . . . . . . 18 (5 ยท 2) = 10
31893, 237, 250, 317decsuc 12710 . . . . . . . . . . . . . . . . 17 ((5 ยท 2) + 1) = 11
319233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318decmac 12731 . . . . . . . . . . . . . . . 16 ((25 ยท 2) + 1) = 51
320233, 310, 231, 311, 233, 93, 319, 255decmul1c 12744 . . . . . . . . . . . . . . 15 (256 ยท 2) = 512
321320a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (256 ยท 2) = 512)
322309, 321eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = 512)
323303, 322eqtrd 2772 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2โ†‘9) = 512)
324323oveq1d 7426 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) = (512 โˆ’ 1))
325 1p1e2 12339 . . . . . . . . . . . . . 14 (1 + 1) = 2
326 eqid 2732 . . . . . . . . . . . . . 14 511 = 511
327272, 93, 325, 326decsuc 12710 . . . . . . . . . . . . 13 (511 + 1) = 512
328272, 233deccl 12694 . . . . . . . . . . . . . . 15 512 โˆˆ โ„•0
329328nn0cni 12486 . . . . . . . . . . . . . 14 512 โˆˆ โ„‚
330272, 93deccl 12694 . . . . . . . . . . . . . . 15 511 โˆˆ โ„•0
331330nn0cni 12486 . . . . . . . . . . . . . 14 511 โˆˆ โ„‚
332329, 242, 331subadd2i 11550 . . . . . . . . . . . . 13 ((512 โˆ’ 1) = 511 โ†” (511 + 1) = 512)
333327, 332mpbir 230 . . . . . . . . . . . 12 (512 โˆ’ 1) = 511
334333a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (512 โˆ’ 1) = 511)
335324, 334eqtr2d 2773 . . . . . . . . . 10 (๐œ‘ โ†’ 511 = ((2โ†‘9) โˆ’ 1))
336279, 295, 3353brtr3d 5179 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < ((2โ†‘9) โˆ’ 1))
337216ltm1d 12148 . . . . . . . . . 10 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘9))
338215nn0zd 12586 . . . . . . . . . . . 12 (๐œ‘ โ†’ 9 โˆˆ โ„ค)
33973, 338, 143, 35leexp2d 14217 . . . . . . . . . . 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 11376 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
342213, 217, 224, 336, 341lttrd 11377 . . . . . . . 8 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
343204, 342eqbrtrd 5170 . . . . . . 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 5170 . . . . 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 7419 . . . . . . . . . . . . 13 (3 = ๐‘ โ†’ (2 logb 3) = (2 logb ๐‘))
348347adantl 482 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
349348oveq1d 7426 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘5) = ((2 logb ๐‘)โ†‘5))
350349fveq2d 6895 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
3518a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ต = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
352351eqcomd 2738 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb ๐‘)โ†‘5)) = ๐ต)
353350, 352eqtrd 2772 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = ๐ต)
354353oveq2d 7427 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) = (2 logb ๐ต))
355354fveq2d 6895 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5)))) = (โŒŠโ€˜(2 logb ๐ต)))
356346, 355oveq12d 7429 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))))
357346oveq2d 7427 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
358357oveq1d 7426 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘2) = ((2 logb ๐‘)โ†‘2))
359358fveq2d 6895 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜((2 logb 3)โ†‘2)) = (โŒŠโ€˜((2 logb ๐‘)โ†‘2)))
360359oveq2d 7427 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2))))
361360prodeq1d 15867 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1))
362356, 361oveq12d 7429 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)))
363350oveq2d 7427 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
364345, 362, 3633brtr3d 5179 . . . 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 2738 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ๐ด)
3678oveq2i 7422 . . . . . 6 (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
368367a1i 11 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
369368eqcomd 2738 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))) = (2โ†‘๐ต))
370364, 366, 3693brtr3d 5179 . . 3 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
371370ex 413 . 2 (๐œ‘ โ†’ (3 = ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
372 eluzle 12837 . . . 4 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ 3 โ‰ค ๐‘)
3733, 372syl 17 . . 3 (๐œ‘ โ†’ 3 โ‰ค ๐‘)
37414zred 12668 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
37555, 374leloed 11359 . . 3 (๐œ‘ โ†’ (3 โ‰ค ๐‘ โ†” (3 < ๐‘ โˆจ 3 = ๐‘)))
376373, 375mpbid 231 . 2 (๐œ‘ โ†’ (3 < ๐‘ โˆจ 3 = ๐‘))
37723, 371, 376mpjaod 858 1 (๐œ‘ โ†’ ๐ด < (2โ†‘๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   class class class wbr 5148  โ€˜cfv 6543  (class class class)co 7411  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   < clt 11250   โ‰ค cle 11251   โˆ’ cmin 11446  โ„•cn 12214  2c2 12269  3c3 12270  4c4 12271  5c5 12272  6c6 12273  7c7 12274  8c8 12275  9c9 12276  โ„•0cn0 12474  โ„คcz 12560  cdc 12679  โ„คโ‰ฅcuz 12824  โ„+crp 12976  ...cfz 13486  โŒŠcfl 13757  โŒˆcceil 13758  โ†‘cexp 14029  โˆcprod 15851   logb clogb 26276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191  ax-mulf 11192
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-div 11874  df-nn 12215  df-2 12277  df-3 12278  df-4 12279  df-5 12280  df-6 12281  df-7 12282  df-8 12283  df-9 12284  df-n0 12475  df-z 12561  df-dec 12680  df-uz 12825  df-q 12935  df-rp 12977  df-xneg 13094  df-xadd 13095  df-xmul 13096  df-ioo 13330  df-ioc 13331  df-ico 13332  df-icc 13333  df-fz 13487  df-fzo 13630  df-fl 13759  df-ceil 13760  df-mod 13837  df-seq 13969  df-exp 14030  df-fac 14236  df-bc 14265  df-hash 14293  df-shft 15016  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-limsup 15417  df-clim 15434  df-rlim 15435  df-sum 15635  df-prod 15852  df-ef 16013  df-e 16014  df-sin 16015  df-cos 16016  df-pi 16018  df-struct 17082  df-sets 17099  df-slot 17117  df-ndx 17129  df-base 17147  df-ress 17176  df-plusg 17212  df-mulr 17213  df-starv 17214  df-sca 17215  df-vsca 17216  df-ip 17217  df-tset 17218  df-ple 17219  df-ds 17221  df-unif 17222  df-hom 17223  df-cco 17224  df-rest 17370  df-topn 17371  df-0g 17389  df-gsum 17390  df-topgen 17391  df-pt 17392  df-prds 17395  df-xrs 17450  df-qtop 17455  df-imas 17456  df-xps 17458  df-mre 17532  df-mrc 17533  df-acs 17535  df-mgm 18563  df-sgrp 18612  df-mnd 18628  df-submnd 18674  df-mulg 18953  df-cntz 19183  df-cmn 19652  df-psmet 20942  df-xmet 20943  df-met 20944  df-bl 20945  df-mopn 20946  df-fbas 20947  df-fg 20948  df-cnfld 20951  df-top 22403  df-topon 22420  df-topsp 22442  df-bases 22456  df-cld 22530  df-ntr 22531  df-cls 22532  df-nei 22609  df-lp 22647  df-perf 22648  df-cn 22738  df-cnp 22739  df-haus 22826  df-cmp 22898  df-tx 23073  df-hmeo 23266  df-fil 23357  df-fm 23449  df-flim 23450  df-flf 23451  df-xms 23833  df-ms 23834  df-tms 23835  df-cncf 24401  df-limc 25390  df-dv 25391  df-log 26072  df-cxp 26073  df-logb 26277
This theorem is referenced by:  aks4d1p3  41029
  Copyright terms: Public domain W3C validator