Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lighneallem2 Structured version   Visualization version   GIF version

Theorem lighneallem2 45302
Description: Lemma 2 for lighneal 45307. (Contributed by AV, 13-Aug-2021.)
Assertion
Ref Expression
lighneallem2 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง 2 โˆฅ ๐‘ โˆง ((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€)) โ†’ ๐‘€ = 1)

Proof of Theorem lighneallem2
Dummy variable ๐‘˜ is distinct from all other variables.
StepHypRef Expression
1 evennn2n 16109 . . . 4 (๐‘ โˆˆ โ„• โ†’ (2 โˆฅ ๐‘ โ†” โˆƒ๐‘˜ โˆˆ โ„• (2 ยท ๐‘˜) = ๐‘))
213ad2ant3 1135 . . 3 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (2 โˆฅ ๐‘ โ†” โˆƒ๐‘˜ โˆˆ โ„• (2 ยท ๐‘˜) = ๐‘))
3 oveq2 7315 . . . . . . . . 9 (๐‘ = (2 ยท ๐‘˜) โ†’ (2โ†‘๐‘) = (2โ†‘(2 ยท ๐‘˜)))
43eqcoms 2744 . . . . . . . 8 ((2 ยท ๐‘˜) = ๐‘ โ†’ (2โ†‘๐‘) = (2โ†‘(2 ยท ๐‘˜)))
5 2cnd 12101 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚)
6 nncn 12031 . . . . . . . . . . . 12 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„‚)
75, 6mulcomd 11046 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ (2 ยท ๐‘˜) = (๐‘˜ ยท 2))
87oveq2d 7323 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (2โ†‘(2 ยท ๐‘˜)) = (2โ†‘(๐‘˜ ยท 2)))
9 2nn0 12300 . . . . . . . . . . . 12 2 โˆˆ โ„•0
109a1i 11 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ 2 โˆˆ โ„•0)
11 nnnn0 12290 . . . . . . . . . . 11 (๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„•0)
125, 10, 11expmuld 13917 . . . . . . . . . 10 (๐‘˜ โˆˆ โ„• โ†’ (2โ†‘(๐‘˜ ยท 2)) = ((2โ†‘๐‘˜)โ†‘2))
138, 12eqtrd 2776 . . . . . . . . 9 (๐‘˜ โˆˆ โ„• โ†’ (2โ†‘(2 ยท ๐‘˜)) = ((2โ†‘๐‘˜)โ†‘2))
1413adantl 483 . . . . . . . 8 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โ†’ (2โ†‘(2 ยท ๐‘˜)) = ((2โ†‘๐‘˜)โ†‘2))
154, 14sylan9eqr 2798 . . . . . . 7 ((((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โˆง (2 ยท ๐‘˜) = ๐‘) โ†’ (2โ†‘๐‘) = ((2โ†‘๐‘˜)โ†‘2))
1615oveq1d 7322 . . . . . 6 ((((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โˆง (2 ยท ๐‘˜) = ๐‘) โ†’ ((2โ†‘๐‘) โˆ’ 1) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ 1))
1716eqeq1d 2738 . . . . 5 ((((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โˆง (2 ยท ๐‘˜) = ๐‘) โ†’ (((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†” (((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€)))
18 elnn1uz2 12715 . . . . . . . 8 (๐‘˜ โˆˆ โ„• โ†” (๐‘˜ = 1 โˆจ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2)))
19 oveq2 7315 . . . . . . . . . . . . . . . . 17 (๐‘˜ = 1 โ†’ (2โ†‘๐‘˜) = (2โ†‘1))
20 2cn 12098 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„‚
21 exp1 13838 . . . . . . . . . . . . . . . . . 18 (2 โˆˆ โ„‚ โ†’ (2โ†‘1) = 2)
2220, 21ax-mp 5 . . . . . . . . . . . . . . . . 17 (2โ†‘1) = 2
2319, 22eqtrdi 2792 . . . . . . . . . . . . . . . 16 (๐‘˜ = 1 โ†’ (2โ†‘๐‘˜) = 2)
2423oveq1d 7322 . . . . . . . . . . . . . . 15 (๐‘˜ = 1 โ†’ ((2โ†‘๐‘˜)โ†‘2) = (2โ†‘2))
2524oveq1d 7322 . . . . . . . . . . . . . 14 (๐‘˜ = 1 โ†’ (((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = ((2โ†‘2) โˆ’ 1))
26 sq2 13964 . . . . . . . . . . . . . . . 16 (2โ†‘2) = 4
2726oveq1i 7317 . . . . . . . . . . . . . . 15 ((2โ†‘2) โˆ’ 1) = (4 โˆ’ 1)
28 4m1e3 12152 . . . . . . . . . . . . . . 15 (4 โˆ’ 1) = 3
2927, 28eqtri 2764 . . . . . . . . . . . . . 14 ((2โ†‘2) โˆ’ 1) = 3
3025, 29eqtrdi 2792 . . . . . . . . . . . . 13 (๐‘˜ = 1 โ†’ (((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = 3)
3130eqeq1d 2738 . . . . . . . . . . . 12 (๐‘˜ = 1 โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†” 3 = (๐‘ƒโ†‘๐‘€)))
3231adantr 482 . . . . . . . . . . 11 ((๐‘˜ = 1 โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†” 3 = (๐‘ƒโ†‘๐‘€)))
33 eqcom 2743 . . . . . . . . . . . . . 14 (3 = (๐‘ƒโ†‘๐‘€) โ†” (๐‘ƒโ†‘๐‘€) = 3)
34 eldifi 4067 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„™)
35 prmnn 16428 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
36 nnre 12030 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„)
3734, 35, 363syl 18 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„)
38373ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘ƒ โˆˆ โ„)
39 nnnn0 12290 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„•0)
40393ad2ant2 1134 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„•0)
4138, 40reexpcld 13931 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ƒโ†‘๐‘€) โˆˆ โ„)
4241adantr 482 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ƒโ†‘๐‘€) = 3) โ†’ (๐‘ƒโ†‘๐‘€) โˆˆ โ„)
43 simpr 486 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ƒโ†‘๐‘€) = 3) โ†’ (๐‘ƒโ†‘๐‘€) = 3)
4442, 43eqled 11128 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘ƒโ†‘๐‘€) = 3) โ†’ (๐‘ƒโ†‘๐‘€) โ‰ค 3)
4544ex 414 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘๐‘€) = 3 โ†’ (๐‘ƒโ†‘๐‘€) โ‰ค 3))
4633, 45syl5bi 242 . . . . . . . . . . . . 13 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (3 = (๐‘ƒโ†‘๐‘€) โ†’ (๐‘ƒโ†‘๐‘€) โ‰ค 3))
4735nnred 12038 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„)
48 prmgt1 16451 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ โ„™ โ†’ 1 < ๐‘ƒ)
4947, 48jca 513 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ))
5034, 49syl 17 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ))
51503ad2ant1 1133 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ))
52 nnz 12392 . . . . . . . . . . . . . . . 16 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„ค)
53523ad2ant2 1134 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„ค)
54 3rp 12786 . . . . . . . . . . . . . . . 16 3 โˆˆ โ„+
5554a1i 11 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 3 โˆˆ โ„+)
56 efexple 26478 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ) โˆง ๐‘€ โˆˆ โ„ค โˆง 3 โˆˆ โ„+) โ†’ ((๐‘ƒโ†‘๐‘€) โ‰ค 3 โ†” ๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ)))))
5751, 53, 55, 56syl3anc 1371 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘๐‘€) โ‰ค 3 โ†” ๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ)))))
58 oddprmge3 16454 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜3))
59 eluzle 12645 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜3) โ†’ 3 โ‰ค ๐‘ƒ)
6058, 59syl 17 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ 3 โ‰ค ๐‘ƒ)
6154a1i 11 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ 3 โˆˆ โ„+)
62 nnrp 12791 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„+)
6334, 35, 623syl 18 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„+)
6461, 63logled 25831 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (3 โ‰ค ๐‘ƒ โ†” (logโ€˜3) โ‰ค (logโ€˜๐‘ƒ)))
6560, 64mpbid 231 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (logโ€˜3) โ‰ค (logโ€˜๐‘ƒ))
66653ad2ant1 1133 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (logโ€˜3) โ‰ค (logโ€˜๐‘ƒ))
67 relogcl 25780 . . . . . . . . . . . . . . . . . 18 (3 โˆˆ โ„+ โ†’ (logโ€˜3) โˆˆ โ„)
6854, 67ax-mp 5 . . . . . . . . . . . . . . . . 17 (logโ€˜3) โˆˆ โ„
69 rplogcl 25808 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„ โˆง 1 < ๐‘ƒ) โ†’ (logโ€˜๐‘ƒ) โˆˆ โ„+)
7034, 49, 693syl 18 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (logโ€˜๐‘ƒ) โˆˆ โ„+)
71703ad2ant1 1133 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (logโ€˜๐‘ƒ) โˆˆ โ„+)
72 divle1le 12850 . . . . . . . . . . . . . . . . 17 (((logโ€˜3) โˆˆ โ„ โˆง (logโ€˜๐‘ƒ) โˆˆ โ„+) โ†’ (((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1 โ†” (logโ€˜3) โ‰ค (logโ€˜๐‘ƒ)))
7368, 71, 72sylancr 588 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1 โ†” (logโ€˜3) โ‰ค (logโ€˜๐‘ƒ)))
7466, 73mpbird 257 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1)
75 fldivle 13601 . . . . . . . . . . . . . . . . 17 (((logโ€˜3) โˆˆ โ„ โˆง (logโ€˜๐‘ƒ) โˆˆ โ„+) โ†’ (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)))
7668, 71, 75sylancr 588 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)))
77 nnre 12030 . . . . . . . . . . . . . . . . . . 19 (๐‘€ โˆˆ โ„• โ†’ ๐‘€ โˆˆ โ„)
78773ad2ant2 1134 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ๐‘€ โˆˆ โ„)
7968a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (logโ€˜3) โˆˆ โ„)
8062relogcld 25827 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„• โ†’ (logโ€˜๐‘ƒ) โˆˆ โ„)
8134, 35, 803syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (logโ€˜๐‘ƒ) โˆˆ โ„)
8235nnrpd 12820 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„+)
83 1red 11026 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„™ โ†’ 1 โˆˆ โ„)
8483, 48gtned 11160 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โ‰  1)
8582, 84jca 513 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ƒ โˆˆ โ„+ โˆง ๐‘ƒ โ‰  1))
86 logne0 25784 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ โ„+ โˆง ๐‘ƒ โ‰  1) โ†’ (logโ€˜๐‘ƒ) โ‰  0)
8734, 85, 863syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (logโ€˜๐‘ƒ) โ‰  0)
8879, 81, 87redivcld 11853 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆˆ โ„)
8988flcld 13568 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆˆ โ„ค)
9089zred 12476 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆˆ โ„)
91903ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆˆ โ„)
92883ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆˆ โ„)
93 letr 11119 . . . . . . . . . . . . . . . . . 18 ((๐‘€ โˆˆ โ„ โˆง (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆˆ โ„ โˆง ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆˆ โ„) โ†’ ((๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆง (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ))) โ†’ ๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ))))
9478, 91, 92, 93syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆง (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ))) โ†’ ๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ))))
95 1red 11026 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ 1 โˆˆ โ„)
96 letr 11119 . . . . . . . . . . . . . . . . . . . 20 ((๐‘€ โˆˆ โ„ โˆง ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆง ((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1) โ†’ ๐‘€ โ‰ค 1))
9778, 92, 95, 96syl3anc 1371 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆง ((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1) โ†’ ๐‘€ โ‰ค 1))
98 nnge1 12051 . . . . . . . . . . . . . . . . . . . . 21 (๐‘€ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘€)
99 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘€ = 1 โ†” 1 = ๐‘€)
100 1red 11026 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘€ โˆˆ โ„• โ†’ 1 โˆˆ โ„)
101100, 77letri3d 11167 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘€ โˆˆ โ„• โ†’ (1 = ๐‘€ โ†” (1 โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค 1)))
10299, 101bitr2id 284 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘€ โˆˆ โ„• โ†’ ((1 โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค 1) โ†” ๐‘€ = 1))
103102biimpd 228 . . . . . . . . . . . . . . . . . . . . 21 (๐‘€ โˆˆ โ„• โ†’ ((1 โ‰ค ๐‘€ โˆง ๐‘€ โ‰ค 1) โ†’ ๐‘€ = 1))
10498, 103mpand 693 . . . . . . . . . . . . . . . . . . . 20 (๐‘€ โˆˆ โ„• โ†’ (๐‘€ โ‰ค 1 โ†’ ๐‘€ = 1))
1051043ad2ant2 1134 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โ‰ค 1 โ†’ ๐‘€ = 1))
10697, 105syld 47 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)) โˆง ((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1) โ†’ ๐‘€ = 1))
107106expd 417 . . . . . . . . . . . . . . . . 17 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ)) โ†’ (((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1 โ†’ ๐‘€ = 1)))
10894, 107syld 47 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โˆง (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ‰ค ((logโ€˜3) / (logโ€˜๐‘ƒ))) โ†’ (((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1 โ†’ ๐‘€ = 1)))
10976, 108mpan2d 692 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ†’ (((logโ€˜3) / (logโ€˜๐‘ƒ)) โ‰ค 1 โ†’ ๐‘€ = 1)))
11074, 109mpid 44 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘€ โ‰ค (โŒŠโ€˜((logโ€˜3) / (logโ€˜๐‘ƒ))) โ†’ ๐‘€ = 1))
11157, 110sylbid 239 . . . . . . . . . . . . 13 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((๐‘ƒโ†‘๐‘€) โ‰ค 3 โ†’ ๐‘€ = 1))
11246, 111syld 47 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (3 = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
113112adantl 483 . . . . . . . . . . 11 ((๐‘˜ = 1 โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ (3 = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
11432, 113sylbid 239 . . . . . . . . . 10 ((๐‘˜ = 1 โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
115114ex 414 . . . . . . . . 9 (๐‘˜ = 1 โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
116 sq1 13962 . . . . . . . . . . . . . 14 (1โ†‘2) = 1
117116eqcomi 2745 . . . . . . . . . . . . 13 1 = (1โ†‘2)
118117oveq2i 7318 . . . . . . . . . . . 12 (((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2))
119118eqeq1i 2741 . . . . . . . . . . 11 ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†” (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) = (๐‘ƒโ†‘๐‘€))
120 eqcom 2743 . . . . . . . . . . . 12 ((((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) = (๐‘ƒโ†‘๐‘€) โ†” (๐‘ƒโ†‘๐‘€) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)))
1219a1i 11 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 2 โˆˆ โ„•0)
122 eluzge2nn0 12677 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘˜ โˆˆ โ„•0)
123121, 122nn0expcld 14011 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (2โ†‘๐‘˜) โˆˆ โ„•0)
124123adantr 482 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ (2โ†‘๐‘˜) โˆˆ โ„•0)
125 1nn0 12299 . . . . . . . . . . . . . . 15 1 โˆˆ โ„•0
126125a1i 11 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ 1 โˆˆ โ„•0)
127 1p1e2 12148 . . . . . . . . . . . . . . . . 17 (1 + 1) = 2
12822eqcomi 2745 . . . . . . . . . . . . . . . . 17 2 = (2โ†‘1)
129127, 128eqtri 2764 . . . . . . . . . . . . . . . 16 (1 + 1) = (2โ†‘1)
130 eluz2gt1 12710 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 1 < ๐‘˜)
131 2re 12097 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ โ„
132131a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 2 โˆˆ โ„)
133 1zzd 12401 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 1 โˆˆ โ„ค)
134 eluzelz 12642 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘˜ โˆˆ โ„ค)
135 1lt2 12194 . . . . . . . . . . . . . . . . . . 19 1 < 2
136135a1i 11 . . . . . . . . . . . . . . . . . 18 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 1 < 2)
137132, 133, 134, 136ltexp2d 14018 . . . . . . . . . . . . . . . . 17 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (1 < ๐‘˜ โ†” (2โ†‘1) < (2โ†‘๐‘˜)))
138130, 137mpbid 231 . . . . . . . . . . . . . . . 16 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (2โ†‘1) < (2โ†‘๐‘˜))
139129, 138eqbrtrid 5116 . . . . . . . . . . . . . . 15 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (1 + 1) < (2โ†‘๐‘˜))
140139adantr 482 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ (1 + 1) < (2โ†‘๐‘˜))
14134, 39anim12i 614 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„•) โ†’ (๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„•0))
1421413adant3 1132 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„•0))
143142adantl 483 . . . . . . . . . . . . . 14 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ (๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„•0))
144 difsqpwdvds 16637 . . . . . . . . . . . . . 14 ((((2โ†‘๐‘˜) โˆˆ โ„•0 โˆง 1 โˆˆ โ„•0 โˆง (1 + 1) < (2โ†‘๐‘˜)) โˆง (๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„•0)) โ†’ ((๐‘ƒโ†‘๐‘€) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) โ†’ ๐‘ƒ โˆฅ (2 ยท 1)))
145124, 126, 140, 143, 144syl31anc 1373 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((๐‘ƒโ†‘๐‘€) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) โ†’ ๐‘ƒ โˆฅ (2 ยท 1)))
146 2t1e2 12186 . . . . . . . . . . . . . . . . . 18 (2 ยท 1) = 2
147146breq2i 5089 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆฅ (2 ยท 1) โ†” ๐‘ƒ โˆฅ 2)
148 prmuz2 16450 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
14934, 148syl 17 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2))
150 2prm 16446 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„™
151 dvdsprm 16457 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง 2 โˆˆ โ„™) โ†’ (๐‘ƒ โˆฅ 2 โ†” ๐‘ƒ = 2))
152149, 150, 151sylancl 587 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆฅ 2 โ†” ๐‘ƒ = 2))
153147, 152bitrid 283 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆฅ (2 ยท 1) โ†” ๐‘ƒ = 2))
154 eldifsn 4726 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†” (๐‘ƒ โˆˆ โ„™ โˆง ๐‘ƒ โ‰  2))
155 eqneqall 2952 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ = 2 โ†’ (๐‘ƒ โ‰  2 โ†’ ๐‘€ = 1))
156155com12 32 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โ‰  2 โ†’ (๐‘ƒ = 2 โ†’ ๐‘€ = 1))
157154, 156simplbiim 506 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ = 2 โ†’ ๐‘€ = 1))
158153, 157sylbid 239 . . . . . . . . . . . . . . 15 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆฅ (2 ยท 1) โ†’ ๐‘€ = 1))
1591583ad2ant1 1133 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (๐‘ƒ โˆฅ (2 ยท 1) โ†’ ๐‘€ = 1))
160159adantl 483 . . . . . . . . . . . . 13 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ (๐‘ƒ โˆฅ (2 ยท 1) โ†’ ๐‘€ = 1))
161145, 160syld 47 . . . . . . . . . . . 12 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((๐‘ƒโ†‘๐‘€) = (((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) โ†’ ๐‘€ = 1))
162120, 161syl5bi 242 . . . . . . . . . . 11 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ (1โ†‘2)) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
163119, 162syl5bi 242 . . . . . . . . . 10 ((๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•)) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
164163ex 414 . . . . . . . . 9 (๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
165115, 164jaoi 855 . . . . . . . 8 ((๐‘˜ = 1 โˆจ ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
16618, 165sylbi 216 . . . . . . 7 (๐‘˜ โˆˆ โ„• โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
167166impcom 409 . . . . . 6 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
168167adantr 482 . . . . 5 ((((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โˆง (2 ยท ๐‘˜) = ๐‘) โ†’ ((((2โ†‘๐‘˜)โ†‘2) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
16917, 168sylbid 239 . . . 4 ((((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง ๐‘˜ โˆˆ โ„•) โˆง (2 ยท ๐‘˜) = ๐‘) โ†’ (((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1))
170169rexlimdva2 3151 . . 3 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (โˆƒ๐‘˜ โˆˆ โ„• (2 ยท ๐‘˜) = ๐‘ โ†’ (((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
1712, 170sylbid 239 . 2 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โ†’ (2 โˆฅ ๐‘ โ†’ (((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€) โ†’ ๐‘€ = 1)))
1721713imp 1111 1 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง 2 โˆฅ ๐‘ โˆง ((2โ†‘๐‘) โˆ’ 1) = (๐‘ƒโ†‘๐‘€)) โ†’ ๐‘€ = 1)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 845   โˆง w3a 1087   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2941  โˆƒwrex 3071   โˆ– cdif 3889  {csn 4565   class class class wbr 5081  โ€˜cfv 6458  (class class class)co 7307  โ„‚cc 10919  โ„cr 10920  0cc0 10921  1c1 10922   + caddc 10924   ยท cmul 10926   < clt 11059   โ‰ค cle 11060   โˆ’ cmin 11255   / cdiv 11682  โ„•cn 12023  2c2 12078  3c3 12079  4c4 12080  โ„•0cn0 12283  โ„คcz 12369  โ„คโ‰ฅcuz 12632  โ„+crp 12780  โŒŠcfl 13560  โ†‘cexp 13832   โˆฅ cdvds 16012  โ„™cprime 16425  logclog 25759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-inf2 9447  ax-cnex 10977  ax-resscn 10978  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-addrcl 10982  ax-mulcl 10983  ax-mulrcl 10984  ax-mulcom 10985  ax-addass 10986  ax-mulass 10987  ax-distr 10988  ax-i2m1 10989  ax-1ne0 10990  ax-1rid 10991  ax-rnegex 10992  ax-rrecex 10993  ax-cnre 10994  ax-pre-lttri 10995  ax-pre-lttrn 10996  ax-pre-ltadd 10997  ax-pre-mulgt0 10998  ax-pre-sup 10999  ax-addf 11000  ax-mulf 11001
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3304  df-reu 3305  df-rab 3306  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-tp 4570  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-iin 4934  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-se 5556  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-isom 6467  df-riota 7264  df-ov 7310  df-oprab 7311  df-mpo 7312  df-of 7565  df-om 7745  df-1st 7863  df-2nd 7864  df-supp 8009  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-1o 8328  df-2o 8329  df-er 8529  df-map 8648  df-pm 8649  df-ixp 8717  df-en 8765  df-dom 8766  df-sdom 8767  df-fin 8768  df-fsupp 9177  df-fi 9218  df-sup 9249  df-inf 9250  df-oi 9317  df-card 9745  df-pnf 11061  df-mnf 11062  df-xr 11063  df-ltxr 11064  df-le 11065  df-sub 11257  df-neg 11258  df-div 11683  df-nn 12024  df-2 12086  df-3 12087  df-4 12088  df-5 12089  df-6 12090  df-7 12091  df-8 12092  df-9 12093  df-n0 12284  df-z 12370  df-dec 12488  df-uz 12633  df-q 12739  df-rp 12781  df-xneg 12898  df-xadd 12899  df-xmul 12900  df-ioo 13133  df-ioc 13134  df-ico 13135  df-icc 13136  df-fz 13290  df-fzo 13433  df-fl 13562  df-mod 13640  df-seq 13772  df-exp 13833  df-fac 14038  df-bc 14067  df-hash 14095  df-shft 14827  df-cj 14859  df-re 14860  df-im 14861  df-sqrt 14995  df-abs 14996  df-limsup 15229  df-clim 15246  df-rlim 15247  df-sum 15447  df-ef 15826  df-sin 15828  df-cos 15829  df-pi 15831  df-dvds 16013  df-gcd 16251  df-prm 16426  df-pc 16587  df-struct 16897  df-sets 16914  df-slot 16932  df-ndx 16944  df-base 16962  df-ress 16991  df-plusg 17024  df-mulr 17025  df-starv 17026  df-sca 17027  df-vsca 17028  df-ip 17029  df-tset 17030  df-ple 17031  df-ds 17033  df-unif 17034  df-hom 17035  df-cco 17036  df-rest 17182  df-topn 17183  df-0g 17201  df-gsum 17202  df-topgen 17203  df-pt 17204  df-prds 17207  df-xrs 17262  df-qtop 17267  df-imas 17268  df-xps 17270  df-mre 17344  df-mrc 17345  df-acs 17347  df-mgm 18375  df-sgrp 18424  df-mnd 18435  df-submnd 18480  df-mulg 18750  df-cntz 18972  df-cmn 19437  df-psmet 20638  df-xmet 20639  df-met 20640  df-bl 20641  df-mopn 20642  df-fbas 20643  df-fg 20644  df-cnfld 20647  df-top 22092  df-topon 22109  df-topsp 22131  df-bases 22145  df-cld 22219  df-ntr 22220  df-cls 22221  df-nei 22298  df-lp 22336  df-perf 22337  df-cn 22427  df-cnp 22428  df-haus 22515  df-tx 22762  df-hmeo 22955  df-fil 23046  df-fm 23138  df-flim 23139  df-flf 23140  df-xms 23522  df-ms 23523  df-tms 23524  df-cncf 24090  df-limc 25079  df-dv 25080  df-log 25761
This theorem is referenced by:  lighneal  45307
  Copyright terms: Public domain W3C validator