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

Theorem nn0prpwlem 35715
Description: Lemma for nn0prpw 35716. Use strong induction to show that every positive integer has unique prime power divisors. (Contributed by Jeff Hankins, 28-Sep-2013.)
Assertion
Ref Expression
nn0prpwlem (๐ด โˆˆ โ„• โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
Distinct variable group:   ๐‘˜,๐‘›,๐‘,๐ด

Proof of Theorem nn0prpwlem
Dummy variables ๐‘š ๐‘ž ๐‘Ÿ ๐‘ก ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5145 . . . 4 (๐‘ฅ = ๐ด โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < ๐ด))
2 breq2 5145 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))
32bibi2d 342 . . . . . 6 (๐‘ฅ = ๐ด โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
43notbid 318 . . . . 5 (๐‘ฅ = ๐ด โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
542rexbidv 3213 . . . 4 (๐‘ฅ = ๐ด โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
61, 5imbi12d 344 . . 3 (๐‘ฅ = ๐ด โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))))
76ralbidv 3171 . 2 (๐‘ฅ = ๐ด โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))))
8 breq2 5145 . . . . 5 (๐‘ฅ = 1 โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < 1))
9 breq2 5145 . . . . . . . 8 (๐‘ฅ = 1 โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))
109bibi2d 342 . . . . . . 7 (๐‘ฅ = 1 โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
1110notbid 318 . . . . . 6 (๐‘ฅ = 1 โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
12112rexbidv 3213 . . . . 5 (๐‘ฅ = 1 โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
138, 12imbi12d 344 . . . 4 (๐‘ฅ = 1 โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))))
1413ralbidv 3171 . . 3 (๐‘ฅ = 1 โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))))
15 breq2 5145 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < ๐‘ฆ))
16 breq2 5145 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))
1716bibi2d 342 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
1817notbid 318 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
19182rexbidv 3213 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
2015, 19imbi12d 344 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))))
2120ralbidv 3171 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))))
22 nnnlt1 12248 . . . . 5 (๐‘˜ โˆˆ โ„• โ†’ ยฌ ๐‘˜ < 1)
2322pm2.21d 121 . . . 4 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
2423rgen 3057 . . 3 โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))
25 exprmfct 16648 . . . 4 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ โˆƒ๐‘ž โˆˆ โ„™ ๐‘ž โˆฅ ๐‘ฅ)
26 prmz 16619 . . . . . . . . . . . . . . . 16 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„ค)
2726adantr 480 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ž โˆˆ โ„ค)
28 prmnn 16618 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„•)
2928nnne0d 12266 . . . . . . . . . . . . . . . 16 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โ‰  0)
3029adantr 480 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ž โ‰  0)
31 nnz 12583 . . . . . . . . . . . . . . . 16 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„ค)
3231adantl 481 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„ค)
33 dvdsval2 16207 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0 โˆง ๐‘ก โˆˆ โ„ค) โ†’ (๐‘ž โˆฅ ๐‘ก โ†” (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3427, 30, 32, 33syl3anc 1368 . . . . . . . . . . . . . 14 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†” (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3534biimpd 228 . . . . . . . . . . . . 13 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
36353ad2antl2 1183 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3736adantrl 713 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
38 simprr 770 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
39 nnre 12223 . . . . . . . . . . . . . . . . . 18 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„)
40 nngt0 12247 . . . . . . . . . . . . . . . . . 18 (๐‘ก โˆˆ โ„• โ†’ 0 < ๐‘ก)
4139, 40jca 511 . . . . . . . . . . . . . . . . 17 (๐‘ก โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก))
42 nnre 12223 . . . . . . . . . . . . . . . . . . 19 (๐‘ž โˆˆ โ„• โ†’ ๐‘ž โˆˆ โ„)
43 nngt0 12247 . . . . . . . . . . . . . . . . . . 19 (๐‘ž โˆˆ โ„• โ†’ 0 < ๐‘ž)
4442, 43jca 511 . . . . . . . . . . . . . . . . . 18 (๐‘ž โˆˆ โ„• โ†’ (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž))
4528, 44syl 17 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ โ„™ โ†’ (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž))
46 divgt0 12086 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก) โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ 0 < (๐‘ก / ๐‘ž))
4741, 45, 46syl2anr 596 . . . . . . . . . . . . . . . 16 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ 0 < (๐‘ก / ๐‘ž))
48473ad2antl2 1183 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ 0 < (๐‘ก / ๐‘ž))
4948adantrr 714 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ 0 < (๐‘ก / ๐‘ž))
50 elnnz 12572 . . . . . . . . . . . . . 14 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†” ((๐‘ก / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ก / ๐‘ž)))
5138, 49, 50sylanbrc 582 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•)
5251expr 456 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•))
5352adantrl 713 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•))
5426adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ž โˆˆ โ„ค)
5529adantr 480 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ž โ‰  0)
56 eluzelz 12836 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„ค)
5756adantl 481 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ฅ โˆˆ โ„ค)
58 dvdsval2 16207 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0 โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) โˆˆ โ„ค))
5954, 55, 57, 58syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) โˆˆ โ„ค))
60 eluzelre 12837 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„)
61 2z 12598 . . . . . . . . . . . . . . . . . . . . . . . 24 2 โˆˆ โ„ค
6261eluz1i 12834 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†” (๐‘ฅ โˆˆ โ„ค โˆง 2 โ‰ค ๐‘ฅ))
63 2pos 12319 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
64 zre 12566 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„)
65 0re 11220 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 โˆˆ โ„
66 2re 12290 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 โˆˆ โ„
67 ltletr 11310 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 โˆˆ โ„ โˆง 2 โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„) โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
6865, 66, 67mp3an12 1447 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ โ„ โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
6964, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ โ„ค โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
7063, 69mpani 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ โ„ค โ†’ (2 โ‰ค ๐‘ฅ โ†’ 0 < ๐‘ฅ))
7170imp 406 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ โ„ค โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ)
7262, 71sylbi 216 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 0 < ๐‘ฅ)
7360, 72jca 511 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ))
74 divgt0 12086 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ) โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ 0 < (๐‘ฅ / ๐‘ž))
7573, 45, 74syl2anr 596 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ 0 < (๐‘ฅ / ๐‘ž))
7675a1d 25 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ 0 < (๐‘ฅ / ๐‘ž)))
7776ancld 550 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ฅ / ๐‘ž))))
78 elnnz 12572 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†” ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ฅ / ๐‘ž)))
7977, 78imbitrrdi 251 . . . . . . . . . . . . . . . . 17 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
8059, 79sylbid 239 . . . . . . . . . . . . . . . 16 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
8180ancoms 458 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
82 breq1 5144 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (๐‘ฆ < ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) < ๐‘ฅ))
83 breq2 5145 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (๐‘˜ < ๐‘ฆ โ†” ๐‘˜ < (๐‘ฅ / ๐‘ž)))
84 breq2 5145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
8584bibi2d 342 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
8685notbid 318 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
87862rexbidv 3213 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
8883, 87imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)) โ†” (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
8988ralbidv 3171 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
9082, 89imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†” ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
9190rspcv 3602 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
92913ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
9392adantl 481 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
94 eluzelcn 12838 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„‚)
9594mullidd 11236 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
9695ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
97 prmgt1 16641 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ž โˆˆ โ„™ โ†’ 1 < ๐‘ž)
9897ad2antlr 724 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 1 < ๐‘ž)
99 1red 11219 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 1 โˆˆ โ„)
10028nnred 12231 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„)
101100ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„)
10260ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ฅ โˆˆ โ„)
10372ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 0 < ๐‘ฅ)
104 ltmul1 12068 . . . . . . . . . . . . . . . . . . . . . 22 ((1 โˆˆ โ„ โˆง ๐‘ž โˆˆ โ„ โˆง (๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ)) โ†’ (1 < ๐‘ž โ†” (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ)))
10599, 101, 102, 103, 104syl112anc 1371 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 < ๐‘ž โ†” (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ)))
10698, 105mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ))
10796, 106eqbrtrrd 5165 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ฅ < (๐‘ž ยท ๐‘ฅ))
10828, 43syl 17 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ž โˆˆ โ„™ โ†’ 0 < ๐‘ž)
109108ad2antlr 724 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 0 < ๐‘ž)
110 ltdivmul 12093 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„ โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†” ๐‘ฅ < (๐‘ž ยท ๐‘ฅ)))
111102, 102, 101, 109, 110syl112anc 1371 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†” ๐‘ฅ < (๐‘ž ยท ๐‘ฅ)))
112107, 111mpbird 257 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ฅ / ๐‘ž) < ๐‘ฅ)
113 breq1 5144 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
114 breq2 5145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
115114bibi1d 343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
116115notbid 318 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
1171162rexbidv 3213 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
118113, 117imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ ((๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†” ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
119118rspcv 3602 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
1201193ad2ant2 1131 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
121120adantl 481 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
122393ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„)
123122adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ก โˆˆ โ„)
124 ltdiv1 12082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ก โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„ โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ (๐‘ก < ๐‘ฅ โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
125123, 102, 101, 109, 124syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
126125biimpa 476 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž))
127 simprll 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ ๐‘ โˆˆ โ„™)
128 peano2nn 12228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
129128adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + 1) โˆˆ โ„•)
130129ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘› + 1) โˆˆ โ„•)
13126ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„ค)
132 nnnn0 12483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
133132ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘› โˆˆ โ„•0)
134 zexpcl 14047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐‘ž โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•0) โ†’ (๐‘žโ†‘๐‘›) โˆˆ โ„ค)
135131, 133, 134syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘žโ†‘๐‘›) โˆˆ โ„ค)
136 nnz 12583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
1371363ad2ant2 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
138137ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
13929ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โ‰  0)
140 dvdsmulcr 16236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐‘žโ†‘๐‘›) โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค โˆง (๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
141135, 138, 131, 139, 140syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
14228nncnd 12232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„‚)
143142ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„‚)
144143, 133expp1d 14117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘žโ†‘(๐‘› + 1)) = ((๐‘žโ†‘๐‘›) ยท ๐‘ž))
145144eqcomd 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) ยท ๐‘ž) = (๐‘žโ†‘(๐‘› + 1)))
146 nncn 12224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„‚)
1471463ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„‚)
148147ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ก โˆˆ โ„‚)
149148, 143, 139divcan1d 11995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) ยท ๐‘ž) = ๐‘ก)
150145, 149breq12d 5154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
151141, 150bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
152 nnz 12583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
1531523ad2ant1 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
154153ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
155 dvdsmulcr 16236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐‘žโ†‘๐‘›) โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง (๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
156135, 154, 131, 139, 155syl112anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
15794ad4antr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ฅ โˆˆ โ„‚)
158157, 143, 139divcan1d 11995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) = ๐‘ฅ)
159145, 158breq12d 5154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
160156, 159bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
161151, 160bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
162161notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
163162biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
164163impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
165 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘š = (๐‘› + 1) โ†’ (๐‘žโ†‘๐‘š) = (๐‘žโ†‘(๐‘› + 1)))
166165breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = (๐‘› + 1) โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
167165breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = (๐‘› + 1) โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
168166, 167bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘š = (๐‘› + 1) โ†’ (((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
169168notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘š = (๐‘› + 1) โ†’ (ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
170169rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐‘› + 1) โˆˆ โ„• โˆง ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
171130, 164, 170syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
172 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘๐‘›) = (๐‘žโ†‘๐‘›))
173172breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
174172breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
175173, 174bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
176175notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
177176anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ = ๐‘ž โ†’ (((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†” ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
178177anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ = ๐‘ž โ†’ (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†” ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
179 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘๐‘š) = (๐‘žโ†‘๐‘š))
180179breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ก))
181179breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
182180, 181bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ = ๐‘ž โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
183182notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
184183rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ = ๐‘ž โ†’ (โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
185178, 184imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ = ๐‘ž โ†’ ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))))
186171, 185mpbiri 258 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ = ๐‘ž โ†’ (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
187186com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
188 simplr 766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž) โ†’ ๐‘› โˆˆ โ„•)
189188ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ๐‘› โˆˆ โ„•)
190 prmz 16619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ โ„ค)
191190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„ค)
192191ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ โˆˆ โ„ค)
193132adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•0)
194193ad2antrl 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘› โˆˆ โ„•0)
195 zexpcl 14047 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((๐‘ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•0) โ†’ (๐‘โ†‘๐‘›) โˆˆ โ„ค)
196192, 194, 195syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆˆ โ„ค)
19726ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„ค)
198137ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
199 dvdsmultr2 16248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
200196, 197, 198, 199syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
201196, 197gcdcomd 16462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) gcd ๐‘ž) = (๐‘ž gcd (๐‘โ†‘๐‘›)))
202 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„™)
203 simprl 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ โˆˆ โ„™)
204 simprr 770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘› โˆˆ โ„•)
205 prmdvdsexpb 16660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” ๐‘ž = ๐‘))
206 equcom 2013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (๐‘ž = ๐‘ โ†” ๐‘ = ๐‘ž)
207205, 206bitrdi 287 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” ๐‘ = ๐‘ž))
208207biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†’ ๐‘ = ๐‘ž))
209202, 203, 204, 208syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†’ ๐‘ = ๐‘ž))
210209con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›)))
211210impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›))
212 simp-4r 781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„™)
213 coprm 16655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((๐‘ž โˆˆ โ„™ โˆง (๐‘โ†‘๐‘›) โˆˆ โ„ค) โ†’ (ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1))
214212, 196, 213syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1))
215211, 214mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1)
216201, 215eqtrd 2766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1)
217 coprmdvds 16597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
218196, 197, 198, 217syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
219216, 218mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
220200, 219impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
221147ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ก โˆˆ โ„‚)
222142ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„‚)
22329ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โ‰  0)
224221, 222, 223divcan2d 11996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž ยท (๐‘ก / ๐‘ž)) = ๐‘ก)
225224breq2d 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
226220, 225bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
227153ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
228 dvdsmultr2 16248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
229196, 197, 227, 228syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
230 coprmdvds 16597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
231196, 197, 227, 230syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
232216, 231mpan2d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
233229, 232impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
23494ad4antr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ฅ โˆˆ โ„‚)
235234, 222, 223divcan2d 11996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) = ๐‘ฅ)
236235breq2d 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
237233, 236bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
238226, 237bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
239238notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
240239biimpa 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
241 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (๐‘š = ๐‘› โ†’ (๐‘โ†‘๐‘š) = (๐‘โ†‘๐‘›))
242241breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
243241breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
244242, 243bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘š = ๐‘› โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
245244notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = ๐‘› โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
246245rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐‘› โˆˆ โ„• โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
247189, 240, 246syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
248247ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
249248expr 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))))
250249com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))))
251250impr 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
252187, 251pm2.61d 179 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
253 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘Ÿ = ๐‘ โ†’ (๐‘Ÿโ†‘๐‘š) = (๐‘โ†‘๐‘š))
254253breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ก))
255253breq1d 5151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
256254, 255bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘Ÿ = ๐‘ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
257256notbid 318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘Ÿ = ๐‘ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
258257rexbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘Ÿ = ๐‘ โ†’ (โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
259258rspcev 3606 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ โˆˆ โ„™ โˆง โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
260127, 252, 259syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
261260exp32 420 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
262261rexlimdvv 3204 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
263126, 262embantd 59 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
264263ex 412 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
265264com23 86 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
266121, 265syld 47 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
267112, 266embantd 59 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
26893, 267syld 47 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
2692683exp2 1351 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))))))
27081, 269syld 47 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))))))
2712703impia 1114 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))))
272271com24 95 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก โˆˆ โ„• โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))))
273272imp32 418 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
27437, 53, 2733syld 60 . . . . . . . . . 10 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
275 simpl2 1189 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ๐‘ž โˆˆ โ„™)
276 1nn 12227 . . . . . . . . . . . . . . 15 1 โˆˆ โ„•
277276a1i 11 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ 1 โˆˆ โ„•)
278142exp1d 14111 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ž โˆˆ โ„™ โ†’ (๐‘žโ†‘1) = ๐‘ž)
279278breq1d 5151 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ž โˆˆ โ„™ โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” ๐‘ž โˆฅ ๐‘ก))
280279notbid 318 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ โ„™ โ†’ (ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก โ†” ยฌ ๐‘ž โˆฅ ๐‘ก))
281280biimpar 477 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ยฌ ๐‘ž โˆฅ ๐‘ก) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
2822813ad2antl2 1183 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ยฌ ๐‘ž โˆฅ ๐‘ก) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
283282adantrr 714 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ)) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
284283adantrl 713 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
285278breq1d 5151 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ โ„™ โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†” ๐‘ž โˆฅ ๐‘ฅ))
286285biimpar 477 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ฅ)
2872863adant1 1127 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ฅ)
288 idd 24 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก) โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก)))
289287, 288mpid 44 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก))
290289adantr 480 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ (((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก))
291284, 290mtod 197 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก))
292 biimpr 219 . . . . . . . . . . . . . . 15 (((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ) โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก))
293291, 292nsyl 140 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ))
294 oveq1 7412 . . . . . . . . . . . . . . . . . 18 (๐‘Ÿ = ๐‘ž โ†’ (๐‘Ÿโ†‘๐‘š) = (๐‘žโ†‘๐‘š))
295294breq1d 5151 . . . . . . . . . . . . . . . . 17 (๐‘Ÿ = ๐‘ž โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ก))
296294breq1d 5151 . . . . . . . . . . . . . . . . 17 (๐‘Ÿ = ๐‘ž โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
297295, 296bibi12d 345 . . . . . . . . . . . . . . . 16 (๐‘Ÿ = ๐‘ž โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
298297notbid 318 . . . . . . . . . . . . . . 15 (๐‘Ÿ = ๐‘ž โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
299 oveq2 7413 . . . . . . . . . . . . . . . . . 18 (๐‘š = 1 โ†’ (๐‘žโ†‘๐‘š) = (๐‘žโ†‘1))
300299breq1d 5151 . . . . . . . . . . . . . . . . 17 (๐‘š = 1 โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ก))
301299breq1d 5151 . . . . . . . . . . . . . . . . 17 (๐‘š = 1 โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ))
302300, 301bibi12d 345 . . . . . . . . . . . . . . . 16 (๐‘š = 1 โ†’ (((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)))
303302notbid 318 . . . . . . . . . . . . . . 15 (๐‘š = 1 โ†’ (ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)))
304298, 303rspc2ev 3619 . . . . . . . . . . . . . 14 ((๐‘ž โˆˆ โ„™ โˆง 1 โˆˆ โ„• โˆง ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
305275, 277, 293, 304syl3anc 1368 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
306305expr 456 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ ((ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
307306expd 415 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ (ยฌ ๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
308307adantrl 713 . . . . . . . . . 10 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (ยฌ ๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
309274, 308pm2.61d 179 . . . . . . . . 9 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
310309expr 456 . . . . . . . 8 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ (๐‘ก โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
311310ralrimiv 3139 . . . . . . 7 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ โˆ€๐‘ก โˆˆ โ„• (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
312 breq1 5144 . . . . . . . . 9 (๐‘ก = ๐‘˜ โ†’ (๐‘ก < ๐‘ฅ โ†” ๐‘˜ < ๐‘ฅ))
313 breq2 5145 . . . . . . . . . . . . 13 (๐‘ก = ๐‘˜ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜))
314313bibi1d 343 . . . . . . . . . . . 12 (๐‘ก = ๐‘˜ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
315314notbid 318 . . . . . . . . . . 11 (๐‘ก = ๐‘˜ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
3163152rexbidv 3213 . . . . . . . . . 10 (๐‘ก = ๐‘˜ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
317253breq1d 5151 . . . . . . . . . . . . 13 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘˜))
318317, 255bibi12d 345 . . . . . . . . . . . 12 (๐‘Ÿ = ๐‘ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
319318notbid 318 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
320241breq1d 5151 . . . . . . . . . . . . 13 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘˜))
321320, 243bibi12d 345 . . . . . . . . . . . 12 (๐‘š = ๐‘› โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
322321notbid 318 . . . . . . . . . . 11 (๐‘š = ๐‘› โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
323319, 322cbvrex2vw 3233 . . . . . . . . . 10 (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
324316, 323bitrdi 287 . . . . . . . . 9 (๐‘ก = ๐‘˜ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
325312, 324imbi12d 344 . . . . . . . 8 (๐‘ก = ๐‘˜ โ†’ ((๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))
326325cbvralvw 3228 . . . . . . 7 (โˆ€๐‘ก โˆˆ โ„• (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
327311, 326sylib 217 . . . . . 6 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
3283273exp1 1349 . . . . 5 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ž โˆˆ โ„™ โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))))
329328rexlimdv 3147 . . . 4 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (โˆƒ๐‘ž โˆˆ โ„™ ๐‘ž โˆฅ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))))
33025, 329mpd 15 . . 3 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))
33114, 21, 24, 330indstr2 12915 . 2 (๐‘ฅ โˆˆ โ„• โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
3327, 331vtoclga 3560 1 (๐ด โˆˆ โ„• โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934  โˆ€wral 3055  โˆƒwrex 3064   class class class wbr 5141  โ€˜cfv 6537  (class class class)co 7405  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   < clt 11252   โ‰ค cle 11253   / cdiv 11875  โ„•cn 12216  2c2 12271  โ„•0cn0 12476  โ„คcz 12562  โ„คโ‰ฅcuz 12826  โ†‘cexp 14032   โˆฅ cdvds 16204   gcd cgcd 16442  โ„™cprime 16615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  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
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-1o 8467  df-2o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12981  df-fz 13491  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-dvds 16205  df-gcd 16443  df-prm 16616
This theorem is referenced by:  nn0prpw  35716
  Copyright terms: Public domain W3C validator