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 40562
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 12239 . . . . . 6 3 โˆˆ โ„•
21a1i 11 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„•)
3 aks4d1p1.1 . . . . . 6 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
43adantr 482 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3))
5 eluznn 12850 . . . . 5 ((3 โˆˆ โ„• โˆง ๐‘ โˆˆ (โ„คโ‰ฅโ€˜3)) โ†’ ๐‘ โˆˆ โ„•)
62, 4, 5syl2anc 585 . . . 4 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ โ„•)
7 aks4d1p1.2 . . . 4 ๐ด = ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1))
8 aks4d1p1.3 . . . 4 ๐ต = (โŒˆโ€˜((2 logb ๐‘)โ†‘5))
9 3p1e4 12305 . . . . 5 (3 + 1) = 4
10 simpr 486 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 < ๐‘)
11 3z 12543 . . . . . . . 8 3 โˆˆ โ„ค
1211a1i 11 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 3 โˆˆ โ„ค)
13 eluzelz 12780 . . . . . . . . 9 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ ๐‘ โˆˆ โ„ค)
143, 13syl 17 . . . . . . . 8 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
1514adantr 482 . . . . . . 7 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐‘ โˆˆ โ„ค)
1612, 15zltp1led 40466 . . . . . 6 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 < ๐‘ โ†” (3 + 1) โ‰ค ๐‘))
1710, 16mpbid 231 . . . . 5 ((๐œ‘ โˆง 3 < ๐‘) โ†’ (3 + 1) โ‰ค ๐‘)
189, 17eqbrtrrid 5146 . . . 4 ((๐œ‘ โˆง 3 < ๐‘) โ†’ 4 โ‰ค ๐‘)
19 eqid 2737 . . . 4 (2 logb (((2 logb ๐‘)โ†‘5) + 1)) = (2 logb (((2 logb ๐‘)โ†‘5) + 1))
20 eqid 2737 . . . 4 ((2 logb ๐‘)โ†‘2) = ((2 logb ๐‘)โ†‘2)
21 eqid 2737 . . . 4 ((2 logb ๐‘)โ†‘4) = ((2 logb ๐‘)โ†‘4)
226, 7, 8, 18, 19, 20, 21aks4d1p1p5 40561 . . 3 ((๐œ‘ โˆง 3 < ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
2322ex 414 . 2 (๐œ‘ โ†’ (3 < ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
24 simp2 1138 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ 3 = ๐‘)
2524eqcomd 2743 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ๐‘ = 3)
2625oveq1d 7377 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ (๐‘โ†‘๐‘˜) = (3โ†‘๐‘˜))
2726oveq1d 7377 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘ โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
28273expa 1119 . . . . . . . 8 (((๐œ‘ โˆง 3 = ๐‘) โˆง ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))) โ†’ ((๐‘โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘๐‘˜) โˆ’ 1))
2928prodeq2dv 15813 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1))
3029oveq2d 7378 . . . . . 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 12927 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
3231a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โˆˆ โ„+)
33 1red 11163 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 โˆˆ โ„)
34 1lt2 12331 . . . . . . . . . . . . . . . . . . 19 1 < 2
3534a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 1 < 2)
3633, 35ltned 11298 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โ‰  2)
3736necomd 3000 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 2 โ‰  1)
3811a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 3 โˆˆ โ„ค)
3932, 37, 38relogbexpd 40460 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = 3)
4039eqcomd 2743 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 3 = (2 logb (2โ†‘3)))
41 cu2 14111 . . . . . . . . . . . . . . . 16 (2โ†‘3) = 8
4241a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘3) = 8)
4342oveq2d 7378 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘3)) = (2 logb 8))
4440, 43eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 3 = (2 logb 8))
45 2z 12542 . . . . . . . . . . . . . . 15 2 โˆˆ โ„ค
4645a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โˆˆ โ„ค)
4746zred 12614 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„)
4847leidd 11728 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค 2)
49 8re 12256 . . . . . . . . . . . . . . 15 8 โˆˆ โ„
5049a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 8 โˆˆ โ„)
51 8pos 12272 . . . . . . . . . . . . . . 15 0 < 8
5251a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 8)
5332rpgt0d 12967 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 2)
54 3re 12240 . . . . . . . . . . . . . . . . . . 19 3 โˆˆ โ„
5554a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 3 โˆˆ โ„)
561nngt0i 12199 . . . . . . . . . . . . . . . . . . 19 0 < 3
5756a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 < 3)
5847, 53, 55, 57, 37relogbcld 40459 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
59 5nn0 12440 . . . . . . . . . . . . . . . . . 18 5 โˆˆ โ„•0
6059a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 5 โˆˆ โ„•0)
6158, 60reexpcld 14075 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
62 ceilcl 13754 . . . . . . . . . . . . . . . 16 (((2 logb 3)โ†‘5) โˆˆ โ„ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
6463zred 12614 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
65 0red 11165 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 0 โˆˆ โ„)
66 9re 12259 . . . . . . . . . . . . . . . . 17 9 โˆˆ โ„
6766a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โˆˆ โ„)
6850lep1d 12093 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 8 โ‰ค (8 + 1))
69 8p1e9 12310 . . . . . . . . . . . . . . . . . 18 (8 + 1) = 9
7069a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (8 + 1) = 9)
7168, 70breqtrd 5136 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 8 โ‰ค 9)
72 2re 12234 . . . . . . . . . . . . . . . . . . . 20 2 โˆˆ โ„
7372a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 2 โˆˆ โ„)
74 2pos 12263 . . . . . . . . . . . . . . . . . . . 20 0 < 2
7574a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 2)
76 3pos 12265 . . . . . . . . . . . . . . . . . . . 20 0 < 3
7776a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 0 < 3)
7873, 75, 55, 77, 37relogbcld 40459 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
7978, 60reexpcld 14075 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
8079, 62syl 17 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
8180zred 12614 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
8255leidd 11728 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ 3 โ‰ค 3)
8355, 823lexlogpow5ineq4 40542 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 9 < ((2 logb 3)โ†‘5))
8467, 79, 83ltled 11310 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 9 โ‰ค ((2 logb 3)โ†‘5))
85 ceilge 13757 . . . . . . . . . . . . . . . . . 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 11319 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 9 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8850, 67, 64, 71, 87letrd 11319 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โ‰ค (โŒˆโ€˜((2 logb 3)โ†‘5)))
8965, 50, 64, 52, 88ltletrd 11322 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
9046, 48, 50, 52, 64, 89, 88logblebd 40462 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb 8) โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9144, 90eqbrtrd 5132 . . . . . . . . . . . 12 (๐œ‘ โ†’ 3 โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))
9279, 33readdcld 11191 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((2 logb 3)โ†‘5) + 1) โˆˆ โ„)
93 1nn0 12436 . . . . . . . . . . . . . . . . . . 19 1 โˆˆ โ„•0
94 6nn 12249 . . . . . . . . . . . . . . . . . . 19 6 โˆˆ โ„•
9593, 94decnncl 12645 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„•
9695a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 16 โˆˆ โ„•)
9796nnred 12175 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 16 โˆˆ โ„)
98 ceilm1lt 13760 . . . . . . . . . . . . . . . . . 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 11758 . . . . . . . . . . . . . . . . 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 40546 . . . . . . . . . . . . . . . . . . 19 ((2 logb 3)โ†‘5) โ‰ค 15
103102a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค 15)
104 5p1e6 12307 . . . . . . . . . . . . . . . . . . . . . 22 (5 + 1) = 6
105 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 15 = 15
10693, 59, 104, 105decsuc 12656 . . . . . . . . . . . . . . . . . . . . 21 (15 + 1) = 16
107106a1i 11 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (15 + 1) = 16)
10897recnd 11190 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 16 โˆˆ โ„‚)
109 1cnd 11157 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
110 5nn 12246 . . . . . . . . . . . . . . . . . . . . . . . 24 5 โˆˆ โ„•
11193, 110decnncl 12645 . . . . . . . . . . . . . . . . . . . . . . 23 15 โˆˆ โ„•
112111a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ 15 โˆˆ โ„•)
113112nncnd 12176 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ 15 โˆˆ โ„‚)
114108, 109, 113subadd2d 11538 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((16 โˆ’ 1) = 15 โ†” (15 + 1) = 16))
115107, 114mpbird 257 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (16 โˆ’ 1) = 15)
116115eqcomd 2743 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 15 = (16 โˆ’ 1))
117103, 116breqtrd 5136 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1))
118 leaddsub 11638 . . . . . . . . . . . . . . . . . 18 ((((2 logb 3)โ†‘5) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง 16 โˆˆ โ„) โ†’ ((((2 logb 3)โ†‘5) + 1) โ‰ค 16 โ†” ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1)))
11979, 33, 97, 118syl3anc 1372 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((((2 logb 3)โ†‘5) + 1) โ‰ค 16 โ†” ((2 logb 3)โ†‘5) โ‰ค (16 โˆ’ 1)))
120117, 119mpbird 257 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((2 logb 3)โ†‘5) + 1) โ‰ค 16)
12181, 92, 97, 101, 120ltletrd 11322 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < 16)
122 eqid 2737 . . . . . . . . . . . . . . . . 17 16 = 16
123 2exp4 16964 . . . . . . . . . . . . . . . . 17 (2โ†‘4) = 16
124122, 123eqtr4i 2768 . . . . . . . . . . . . . . . 16 16 = (2โ†‘4)
125124a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 16 = (2โ†‘4))
126121, 125breqtrd 5136 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) < (2โ†‘4))
12746uzidd 12786 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜2))
12864, 89elrpd 12961 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„+)
129 4z 12544 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„ค
130129a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 4 โˆˆ โ„ค)
13132, 130rpexpcld 14157 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2โ†‘4) โˆˆ โ„+)
132 logblt 26150 . . . . . . . . . . . . . . 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 1372 . . . . . . . . . . . . . 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 40460 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = 4)
1369eqcomi 2746 . . . . . . . . . . . . . . 15 4 = (3 + 1)
137136a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 = (3 + 1))
138135, 137eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 logb (2โ†‘4)) = (3 + 1))
139134, 138breqtrd 5136 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) < (3 + 1))
14091, 139jca 513 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 โ‰ค (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) โˆง (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) < (3 + 1)))
14173, 75, 55, 57, 37relogbcld 40459 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2 logb 3) โˆˆ โ„)
142141, 60reexpcld 14075 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘5) โˆˆ โ„)
143142, 62syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค)
144143zred 12614 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„)
145 9pos 12273 . . . . . . . . . . . . . . 15 0 < 9
146145a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 0 < 9)
14765, 67, 144, 146, 87ltletrd 11322 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 < (โŒˆโ€˜((2 logb 3)โ†‘5)))
14873, 75, 144, 147, 37relogbcld 40459 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
149 flbi 13728 . . . . . . . . . . . 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 585 . . . . . . . . . . 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 257 . . . . . . . . . 10 (๐œ‘ โ†’ (โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5)))) = 3)
152151oveq2d 7378 . . . . . . . . 9 (๐œ‘ โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (3โ†‘3))
15378resqcld 14037 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
154 3lexlogpow2ineq2 40545 . . . . . . . . . . . . . . . . 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 496 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 < ((2 logb 3)โ†‘2))
15773, 153, 156ltled 11310 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 2 โ‰ค ((2 logb 3)โ†‘2))
158155simprd 497 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < 3)
159 df-3 12224 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
160159a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 3 = (2 + 1))
161158, 160breqtrd 5136 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) < (2 + 1))
162157, 161jca 513 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 โ‰ค ((2 logb 3)โ†‘2) โˆง ((2 logb 3)โ†‘2) < (2 + 1)))
163141resqcld 14037 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 logb 3)โ†‘2) โˆˆ โ„)
164 flbi 13728 . . . . . . . . . . . . . 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 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โŒŠโ€˜((2 logb 3)โ†‘2)) = 2 โ†” (2 โ‰ค ((2 logb 3)โ†‘2) โˆง ((2 logb 3)โ†‘2) < (2 + 1))))
166162, 165mpbird 257 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒŠโ€˜((2 logb 3)โ†‘2)) = 2)
167166oveq2d 7378 . . . . . . . . . . 11 (๐œ‘ โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...2))
168167prodeq1d 15811 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1))
169 1zzd 12541 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
170169, 46jca 513 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค))
171 1le2 12369 . . . . . . . . . . . . . . 15 1 โ‰ค 2
172171a1i 11 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 1 โ‰ค 2)
173 eluz 12784 . . . . . . . . . . . . . 14 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ (2 โˆˆ (โ„คโ‰ฅโ€˜1) โ†” 1 โ‰ค 2))
174172, 173mpbird 257 . . . . . . . . . . . . 13 ((1 โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
175170, 174syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 โˆˆ (โ„คโ‰ฅโ€˜1))
176 3cn 12241 . . . . . . . . . . . . . . 15 3 โˆˆ โ„‚
177176a1i 11 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 3 โˆˆ โ„‚)
178 elfznn 13477 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (1...2) โ†’ ๐‘˜ โˆˆ โ„•)
179178adantl 483 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•)
180179nnnn0d 12480 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ๐‘˜ โˆˆ โ„•0)
181177, 180expcld 14058 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ (3โ†‘๐‘˜) โˆˆ โ„‚)
182 1cnd 11157 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ 1 โˆˆ โ„‚)
183181, 182subcld 11519 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘˜ โˆˆ (1...2)) โ†’ ((3โ†‘๐‘˜) โˆ’ 1) โˆˆ โ„‚)
184 oveq2 7370 . . . . . . . . . . . . 13 (๐‘˜ = 2 โ†’ (3โ†‘๐‘˜) = (3โ†‘2))
185184oveq1d 7377 . . . . . . . . . . . 12 (๐‘˜ = 2 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘2) โˆ’ 1))
186175, 183, 185fprodm1 15857 . . . . . . . . . . 11 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
187 2m1e1 12286 . . . . . . . . . . . . . . . 16 (2 โˆ’ 1) = 1
188187a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (2 โˆ’ 1) = 1)
189188oveq2d 7378 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1...(2 โˆ’ 1)) = (1...1))
190189prodeq1d 15811 . . . . . . . . . . . . 13 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...1)((3โ†‘๐‘˜) โˆ’ 1))
19155recnd 11190 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
19293a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โˆˆ โ„•0)
193191, 192expcld 14058 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„‚)
194193, 109subcld 11519 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚)
195169, 194jca 513 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (1 โˆˆ โ„ค โˆง ((3โ†‘1) โˆ’ 1) โˆˆ โ„‚))
196 oveq2 7370 . . . . . . . . . . . . . . . 16 (๐‘˜ = 1 โ†’ (3โ†‘๐‘˜) = (3โ†‘1))
197196oveq1d 7377 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ ((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
198197fprod1 15853 . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . 12 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) = ((3โ†‘1) โˆ’ 1))
201200oveq1d 7377 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆ๐‘˜ โˆˆ (1...(2 โˆ’ 1))((3โ†‘๐‘˜) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
202186, 201eqtrd 2777 . . . . . . . . . 10 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...2)((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
203168, 202eqtrd 2777 . . . . . . . . 9 (๐œ‘ โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
204152, 203oveq12d 7380 . . . . . . . 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 12438 . . . . . . . . . . . 12 3 โˆˆ โ„•0
206205a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 3 โˆˆ โ„•0)
20755, 206reexpcld 14075 . . . . . . . . . 10 (๐œ‘ โ†’ (3โ†‘3) โˆˆ โ„)
20855, 192reexpcld 14075 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘1) โˆˆ โ„)
209208, 33resubcld 11590 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) โˆˆ โ„)
21055resqcld 14037 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘2) โˆˆ โ„)
211210, 33resubcld 11590 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) โˆˆ โ„)
212209, 211remulcld 11192 . . . . . . . . . 10 (๐œ‘ โ†’ (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)) โˆˆ โ„)
213207, 212remulcld 11192 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) โˆˆ โ„)
214 9nn0 12444 . . . . . . . . . . . 12 9 โˆˆ โ„•0
215214a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 9 โˆˆ โ„•0)
21673, 215reexpcld 14075 . . . . . . . . . 10 (๐œ‘ โ†’ (2โ†‘9) โˆˆ โ„)
217216, 33resubcld 11590 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) โˆˆ โ„)
218 elnnz 12516 . . . . . . . . . . . . 13 ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โ†” ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„ค โˆง 0 < (โŒˆโ€˜((2 logb 3)โ†‘5))))
219143, 147, 218sylanbrc 584 . . . . . . . . . . . 12 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„•)
220219orcd 872 . . . . . . . . . . 11 (๐œ‘ โ†’ ((โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„• โˆจ (โŒˆโ€˜((2 logb 3)โ†‘5)) = 0))
221 elnn0 12422 . . . . . . . . . . . 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 257 . . . . . . . . . 10 (๐œ‘ โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) โˆˆ โ„•0)
22473, 223reexpcld 14075 . . . . . . . . 9 (๐œ‘ โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) โˆˆ โ„)
225 8cn 12257 . . . . . . . . . . . . . . 15 8 โˆˆ โ„‚
226 2cn 12235 . . . . . . . . . . . . . . 15 2 โˆˆ โ„‚
227 8t2e16 12740 . . . . . . . . . . . . . . 15 (8 ยท 2) = 16
228225, 226, 227mulcomli 11171 . . . . . . . . . . . . . 14 (2 ยท 8) = 16
229228a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท 8) = 16)
230229oveq2d 7378 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = (27 ยท 16))
231 6nn0 12441 . . . . . . . . . . . . . . 15 6 โˆˆ โ„•0
23293, 231deccl 12640 . . . . . . . . . . . . . 14 16 โˆˆ โ„•0
233 2nn0 12437 . . . . . . . . . . . . . 14 2 โˆˆ โ„•0
234 7nn0 12442 . . . . . . . . . . . . . 14 7 โˆˆ โ„•0
235 eqid 2737 . . . . . . . . . . . . . 14 27 = 27
23693, 93deccl 12640 . . . . . . . . . . . . . 14 11 โˆˆ โ„•0
237 0nn0 12435 . . . . . . . . . . . . . . 15 0 โˆˆ โ„•0
238233dec0h 12647 . . . . . . . . . . . . . . 15 2 = 02
239 eqid 2737 . . . . . . . . . . . . . . 15 11 = 11
240232nn0cni 12432 . . . . . . . . . . . . . . . . . 18 16 โˆˆ โ„‚
241240mul02i 11351 . . . . . . . . . . . . . . . . 17 (0 ยท 16) = 0
242 ax-1cn 11116 . . . . . . . . . . . . . . . . . 18 1 โˆˆ โ„‚
243176, 242, 9addcomli 11354 . . . . . . . . . . . . . . . . 17 (1 + 3) = 4
244241, 243oveq12i 7374 . . . . . . . . . . . . . . . 16 ((0 ยท 16) + (1 + 3)) = (0 + 4)
245 4cn 12245 . . . . . . . . . . . . . . . . 17 4 โˆˆ โ„‚
246245addid2i 11350 . . . . . . . . . . . . . . . 16 (0 + 4) = 4
247244, 246eqtri 2765 . . . . . . . . . . . . . . 15 ((0 ยท 16) + (1 + 3)) = 4
24893dec0h 12647 . . . . . . . . . . . . . . . 16 1 = 01
249 2t1e2 12323 . . . . . . . . . . . . . . . . . 18 (2 ยท 1) = 2
250 0p1e1 12282 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
251249, 250oveq12i 7374 . . . . . . . . . . . . . . . . 17 ((2 ยท 1) + (0 + 1)) = (2 + 1)
252 2p1e3 12302 . . . . . . . . . . . . . . . . 17 (2 + 1) = 3
253251, 252eqtri 2765 . . . . . . . . . . . . . . . 16 ((2 ยท 1) + (0 + 1)) = 3
254 6cn 12251 . . . . . . . . . . . . . . . . . 18 6 โˆˆ โ„‚
255 6t2e12 12729 . . . . . . . . . . . . . . . . . 18 (6 ยท 2) = 12
256254, 226, 255mulcomli 11171 . . . . . . . . . . . . . . . . 17 (2 ยท 6) = 12
25793, 233, 252, 256decsuc 12656 . . . . . . . . . . . . . . . 16 ((2 ยท 6) + 1) = 13
25893, 231, 237, 93, 122, 248, 233, 205, 93, 253, 257decma2c 12678 . . . . . . . . . . . . . . 15 ((2 ยท 16) + 1) = 33
259237, 233, 93, 93, 238, 239, 232, 205, 205, 247, 258decmac 12677 . . . . . . . . . . . . . 14 ((2 ยท 16) + 11) = 43
260 4nn0 12439 . . . . . . . . . . . . . . 15 4 โˆˆ โ„•0
261 7cn 12254 . . . . . . . . . . . . . . . . . 18 7 โˆˆ โ„‚
262261mulid1i 11166 . . . . . . . . . . . . . . . . 17 (7 ยท 1) = 7
263262oveq1i 7372 . . . . . . . . . . . . . . . 16 ((7 ยท 1) + 4) = (7 + 4)
264 7p4e11 12701 . . . . . . . . . . . . . . . 16 (7 + 4) = 11
265263, 264eqtri 2765 . . . . . . . . . . . . . . 15 ((7 ยท 1) + 4) = 11
266 7t6e42 12738 . . . . . . . . . . . . . . 15 (7 ยท 6) = 42
267234, 93, 231, 122, 233, 260, 265, 266decmul2c 12691 . . . . . . . . . . . . . 14 (7 ยท 16) = 112
268232, 233, 234, 235, 233, 236, 259, 267decmul1c 12690 . . . . . . . . . . . . 13 (27 ยท 16) = 432
269268a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (27 ยท 16) = 432)
270230, 269eqtrd 2777 . . . . . . . . . . 11 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = 432)
271260, 205deccl 12640 . . . . . . . . . . . . 13 43 โˆˆ โ„•0
27259, 93deccl 12640 . . . . . . . . . . . . 13 51 โˆˆ โ„•0
273 2lt10 12763 . . . . . . . . . . . . 13 2 < 10
274 3lt10 12762 . . . . . . . . . . . . . 14 3 < 10
275 4lt5 12337 . . . . . . . . . . . . . 14 4 < 5
276260, 59, 205, 93, 274, 275decltc 12654 . . . . . . . . . . . . 13 43 < 51
277271, 272, 233, 93, 273, 276decltc 12654 . . . . . . . . . . . 12 432 < 511
278277a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 432 < 511)
279270, 278eqbrtrd 5132 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) < 511)
280 3exp3 16971 . . . . . . . . . . . . 13 (3โ†‘3) = 27
281280a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3โ†‘3) = 27)
282281eqcomd 2743 . . . . . . . . . . 11 (๐œ‘ โ†’ 27 = (3โ†‘3))
283191exp1d 14053 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘1) = 3)
284283oveq1d 7377 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘1) โˆ’ 1) = (3 โˆ’ 1))
285 3m1e2 12288 . . . . . . . . . . . . . 14 (3 โˆ’ 1) = 2
286285a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 โˆ’ 1) = 2)
287284, 286eqtr2d 2778 . . . . . . . . . . . 12 (๐œ‘ โ†’ 2 = ((3โ†‘1) โˆ’ 1))
288 sq3 14109 . . . . . . . . . . . . . . 15 (3โ†‘2) = 9
289288a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3โ†‘2) = 9)
290289oveq1d 7377 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3โ†‘2) โˆ’ 1) = (9 โˆ’ 1))
291 9m1e8 12294 . . . . . . . . . . . . . 14 (9 โˆ’ 1) = 8
292291a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (9 โˆ’ 1) = 8)
293290, 292eqtr2d 2778 . . . . . . . . . . . 12 (๐œ‘ โ†’ 8 = ((3โ†‘2) โˆ’ 1))
294287, 293oveq12d 7380 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท 8) = (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1)))
295282, 294oveq12d 7380 . . . . . . . . . 10 (๐œ‘ โ†’ (27 ยท (2 ยท 8)) = ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))))
296 df-9 12230 . . . . . . . . . . . . . . . 16 9 = (8 + 1)
297296a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 9 = (8 + 1))
298297oveq2d 7378 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘9) = (2โ†‘(8 + 1)))
299287, 194eqeltrd 2838 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
300 8nn0 12443 . . . . . . . . . . . . . . . 16 8 โˆˆ โ„•0
301300a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ 8 โˆˆ โ„•0)
302299, 192, 301expaddd 14060 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (2โ†‘(8 + 1)) = ((2โ†‘8) ยท (2โ†‘1)))
303298, 302eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2โ†‘9) = ((2โ†‘8) ยท (2โ†‘1)))
304 2exp8 16968 . . . . . . . . . . . . . . . . 17 (2โ†‘8) = 256
305304a1i 11 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘8) = 256)
306305oveq1d 7377 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท (2โ†‘1)))
307299exp1d 14053 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (2โ†‘1) = 2)
308307oveq2d 7378 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (256 ยท (2โ†‘1)) = (256 ยท 2))
309306, 308eqtrd 2777 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = (256 ยท 2))
310233, 59deccl 12640 . . . . . . . . . . . . . . . 16 25 โˆˆ โ„•0
311 eqid 2737 . . . . . . . . . . . . . . . 16 256 = 256
312 eqid 2737 . . . . . . . . . . . . . . . . 17 25 = 25
313 2t2e4 12324 . . . . . . . . . . . . . . . . . . 19 (2 ยท 2) = 4
314313, 250oveq12i 7374 . . . . . . . . . . . . . . . . . 18 ((2 ยท 2) + (0 + 1)) = (4 + 1)
315 4p1e5 12306 . . . . . . . . . . . . . . . . . 18 (4 + 1) = 5
316314, 315eqtri 2765 . . . . . . . . . . . . . . . . 17 ((2 ยท 2) + (0 + 1)) = 5
317 5t2e10 12725 . . . . . . . . . . . . . . . . . 18 (5 ยท 2) = 10
31893, 237, 250, 317decsuc 12656 . . . . . . . . . . . . . . . . 17 ((5 ยท 2) + 1) = 11
319233, 59, 237, 93, 312, 248, 233, 93, 93, 316, 318decmac 12677 . . . . . . . . . . . . . . . 16 ((25 ยท 2) + 1) = 51
320233, 310, 231, 311, 233, 93, 319, 255decmul1c 12690 . . . . . . . . . . . . . . 15 (256 ยท 2) = 512
321320a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (256 ยท 2) = 512)
322309, 321eqtrd 2777 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((2โ†‘8) ยท (2โ†‘1)) = 512)
323303, 322eqtrd 2777 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2โ†‘9) = 512)
324323oveq1d 7377 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) = (512 โˆ’ 1))
325 1p1e2 12285 . . . . . . . . . . . . . 14 (1 + 1) = 2
326 eqid 2737 . . . . . . . . . . . . . 14 511 = 511
327272, 93, 325, 326decsuc 12656 . . . . . . . . . . . . 13 (511 + 1) = 512
328272, 233deccl 12640 . . . . . . . . . . . . . . 15 512 โˆˆ โ„•0
329328nn0cni 12432 . . . . . . . . . . . . . 14 512 โˆˆ โ„‚
330272, 93deccl 12640 . . . . . . . . . . . . . . 15 511 โˆˆ โ„•0
331330nn0cni 12432 . . . . . . . . . . . . . 14 511 โˆˆ โ„‚
332329, 242, 331subadd2i 11496 . . . . . . . . . . . . 13 ((512 โˆ’ 1) = 511 โ†” (511 + 1) = 512)
333327, 332mpbir 230 . . . . . . . . . . . 12 (512 โˆ’ 1) = 511
334333a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (512 โˆ’ 1) = 511)
335324, 334eqtr2d 2778 . . . . . . . . . 10 (๐œ‘ โ†’ 511 = ((2โ†‘9) โˆ’ 1))
336279, 295, 3353brtr3d 5141 . . . . . . . . 9 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < ((2โ†‘9) โˆ’ 1))
337216ltm1d 12094 . . . . . . . . . 10 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘9))
338215nn0zd 12532 . . . . . . . . . . . 12 (๐œ‘ โ†’ 9 โˆˆ โ„ค)
33973, 338, 143, 35leexp2d 14162 . . . . . . . . . . 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 11322 . . . . . . . . 9 (๐œ‘ โ†’ ((2โ†‘9) โˆ’ 1) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
342213, 217, 224, 336, 341lttrd 11323 . . . . . . . 8 (๐œ‘ โ†’ ((3โ†‘3) ยท (((3โ†‘1) โˆ’ 1) ยท ((3โ†‘2) โˆ’ 1))) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
343204, 342eqbrtrd 5132 . . . . . . 7 (๐œ‘ โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
344343adantr 482 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((3โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
34530, 344eqbrtrd 5132 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) < (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))))
346 simpr 486 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ 3 = ๐‘)
347 oveq2 7370 . . . . . . . . . . . . 13 (3 = ๐‘ โ†’ (2 logb 3) = (2 logb ๐‘))
348347adantl 483 . . . . . . . . . . . 12 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
349348oveq1d 7377 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘5) = ((2 logb ๐‘)โ†‘5))
350349fveq2d 6851 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
3518a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ต = (โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
352351eqcomd 2743 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb ๐‘)โ†‘5)) = ๐ต)
353350, 352eqtrd 2777 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒˆโ€˜((2 logb 3)โ†‘5)) = ๐ต)
354353oveq2d 7378 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))) = (2 logb ๐ต))
355354fveq2d 6851 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5)))) = (โŒŠโ€˜(2 logb ๐ต)))
356346, 355oveq12d 7380 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) = (๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))))
357346oveq2d 7378 . . . . . . . . . 10 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2 logb 3) = (2 logb ๐‘))
358357oveq1d 7377 . . . . . . . . 9 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((2 logb 3)โ†‘2) = ((2 logb ๐‘)โ†‘2))
359358fveq2d 6851 . . . . . . . 8 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (โŒŠโ€˜((2 logb 3)โ†‘2)) = (โŒŠโ€˜((2 logb ๐‘)โ†‘2)))
360359oveq2d 7378 . . . . . . 7 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (1...(โŒŠโ€˜((2 logb 3)โ†‘2))) = (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2))))
361360prodeq1d 15811 . . . . . 6 ((๐œ‘ โˆง 3 = ๐‘) โ†’ โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1) = โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1))
362356, 361oveq12d 7380 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((3โ†‘(โŒŠโ€˜(2 logb (โŒˆโ€˜((2 logb 3)โ†‘5))))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb 3)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)))
363350oveq2d 7378 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb 3)โ†‘5))) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
364345, 362, 3633brtr3d 5141 . . . 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 2743 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ((๐‘โ†‘(โŒŠโ€˜(2 logb ๐ต))) ยท โˆ๐‘˜ โˆˆ (1...(โŒŠโ€˜((2 logb ๐‘)โ†‘2)))((๐‘โ†‘๐‘˜) โˆ’ 1)) = ๐ด)
3678oveq2i 7373 . . . . . 6 (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5)))
368367a1i 11 . . . . 5 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘๐ต) = (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))))
369368eqcomd 2743 . . . 4 ((๐œ‘ โˆง 3 = ๐‘) โ†’ (2โ†‘(โŒˆโ€˜((2 logb ๐‘)โ†‘5))) = (2โ†‘๐ต))
370364, 366, 3693brtr3d 5141 . . 3 ((๐œ‘ โˆง 3 = ๐‘) โ†’ ๐ด < (2โ†‘๐ต))
371370ex 414 . 2 (๐œ‘ โ†’ (3 = ๐‘ โ†’ ๐ด < (2โ†‘๐ต)))
372 eluzle 12783 . . . 4 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ 3 โ‰ค ๐‘)
3733, 372syl 17 . . 3 (๐œ‘ โ†’ 3 โ‰ค ๐‘)
37414zred 12614 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
37555, 374leloed 11305 . . 3 (๐œ‘ โ†’ (3 โ‰ค ๐‘ โ†” (3 < ๐‘ โˆจ 3 = ๐‘)))
376373, 375mpbid 231 . 2 (๐œ‘ โ†’ (3 < ๐‘ โˆจ 3 = ๐‘))
37723, 371, 376mpjaod 859 1 (๐œ‘ โ†’ ๐ด < (2โ†‘๐ต))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   class class class wbr 5110  โ€˜cfv 6501  (class class class)co 7362  โ„‚cc 11056  โ„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   ยท cmul 11063   < clt 11196   โ‰ค cle 11197   โˆ’ cmin 11392  โ„•cn 12160  2c2 12215  3c3 12216  4c4 12217  5c5 12218  6c6 12219  7c7 12220  8c8 12221  9c9 12222  โ„•0cn0 12420  โ„คcz 12506  cdc 12625  โ„คโ‰ฅcuz 12770  โ„+crp 12922  ...cfz 13431  โŒŠcfl 13702  โŒˆcceil 13703  โ†‘cexp 13974  โˆcprod 15795   logb clogb 26130
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-ceil 13705  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-prod 15796  df-ef 15957  df-e 15958  df-sin 15959  df-cos 15960  df-pi 15962  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-cxp 25929  df-logb 26131
This theorem is referenced by:  aks4d1p3  40564
  Copyright terms: Public domain W3C validator