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 35195
Description: Lemma for nn0prpw 35196. 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 5151 . . . 4 (๐‘ฅ = ๐ด โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < ๐ด))
2 breq2 5151 . . . . . . 7 (๐‘ฅ = ๐ด โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))
32bibi2d 342 . . . . . 6 (๐‘ฅ = ๐ด โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
43notbid 317 . . . . 5 (๐‘ฅ = ๐ด โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
542rexbidv 3219 . . . 4 (๐‘ฅ = ๐ด โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
61, 5imbi12d 344 . . 3 (๐‘ฅ = ๐ด โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))))
76ralbidv 3177 . 2 (๐‘ฅ = ๐ด โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด))))
8 breq2 5151 . . . . 5 (๐‘ฅ = 1 โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < 1))
9 breq2 5151 . . . . . . . 8 (๐‘ฅ = 1 โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))
109bibi2d 342 . . . . . . 7 (๐‘ฅ = 1 โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
1110notbid 317 . . . . . 6 (๐‘ฅ = 1 โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
12112rexbidv 3219 . . . . 5 (๐‘ฅ = 1 โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
138, 12imbi12d 344 . . . 4 (๐‘ฅ = 1 โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))))
1413ralbidv 3177 . . 3 (๐‘ฅ = 1 โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))))
15 breq2 5151 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘˜ < ๐‘ฅ โ†” ๐‘˜ < ๐‘ฆ))
16 breq2 5151 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))
1716bibi2d 342 . . . . . . 7 (๐‘ฅ = ๐‘ฆ โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
1817notbid 317 . . . . . 6 (๐‘ฅ = ๐‘ฆ โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
19182rexbidv 3219 . . . . 5 (๐‘ฅ = ๐‘ฆ โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))
2015, 19imbi12d 344 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))))
2120ralbidv 3177 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))))
22 nnnlt1 12240 . . . . 5 (๐‘˜ โˆˆ โ„• โ†’ ยฌ ๐‘˜ < 1)
2322pm2.21d 121 . . . 4 (๐‘˜ โˆˆ โ„• โ†’ (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1)))
2423rgen 3063 . . 3 โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < 1 โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ 1))
25 exprmfct 16637 . . . 4 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ โˆƒ๐‘ž โˆˆ โ„™ ๐‘ž โˆฅ ๐‘ฅ)
26 prmz 16608 . . . . . . . . . . . . . . . 16 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„ค)
2726adantr 481 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ž โˆˆ โ„ค)
28 prmnn 16607 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„•)
2928nnne0d 12258 . . . . . . . . . . . . . . . 16 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โ‰  0)
3029adantr 481 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ž โ‰  0)
31 nnz 12575 . . . . . . . . . . . . . . . 16 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„ค)
3231adantl 482 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„ค)
33 dvdsval2 16196 . . . . . . . . . . . . . . 15 ((๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0 โˆง ๐‘ก โˆˆ โ„ค) โ†’ (๐‘ž โˆฅ ๐‘ก โ†” (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3427, 30, 32, 33syl3anc 1371 . . . . . . . . . . . . . 14 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†” (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3534biimpd 228 . . . . . . . . . . . . 13 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
36353ad2antl2 1186 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
3736adantrl 714 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค))
38 simprr 771 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
39 nnre 12215 . . . . . . . . . . . . . . . . . 18 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„)
40 nngt0 12239 . . . . . . . . . . . . . . . . . 18 (๐‘ก โˆˆ โ„• โ†’ 0 < ๐‘ก)
4139, 40jca 512 . . . . . . . . . . . . . . . . 17 (๐‘ก โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก))
42 nnre 12215 . . . . . . . . . . . . . . . . . . 19 (๐‘ž โˆˆ โ„• โ†’ ๐‘ž โˆˆ โ„)
43 nngt0 12239 . . . . . . . . . . . . . . . . . . 19 (๐‘ž โˆˆ โ„• โ†’ 0 < ๐‘ž)
4442, 43jca 512 . . . . . . . . . . . . . . . . . 18 (๐‘ž โˆˆ โ„• โ†’ (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž))
4528, 44syl 17 . . . . . . . . . . . . . . . . 17 (๐‘ž โˆˆ โ„™ โ†’ (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž))
46 divgt0 12078 . . . . . . . . . . . . . . . . 17 (((๐‘ก โˆˆ โ„ โˆง 0 < ๐‘ก) โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ 0 < (๐‘ก / ๐‘ž))
4741, 45, 46syl2anr 597 . . . . . . . . . . . . . . . 16 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ก โˆˆ โ„•) โ†’ 0 < (๐‘ก / ๐‘ž))
48473ad2antl2 1186 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ 0 < (๐‘ก / ๐‘ž))
4948adantrr 715 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ 0 < (๐‘ก / ๐‘ž))
50 elnnz 12564 . . . . . . . . . . . . . 14 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†” ((๐‘ก / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ก / ๐‘ž)))
5138, 49, 50sylanbrc 583 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•)
5251expr 457 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•))
5352adantrl 714 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„•))
5426adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ž โˆˆ โ„ค)
5529adantr 481 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ž โ‰  0)
56 eluzelz 12828 . . . . . . . . . . . . . . . . . . 19 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„ค)
5756adantl 482 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ๐‘ฅ โˆˆ โ„ค)
58 dvdsval2 16196 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0 โˆง ๐‘ฅ โˆˆ โ„ค) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) โˆˆ โ„ค))
5954, 55, 57, 58syl3anc 1371 . . . . . . . . . . . . . . . . 17 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) โˆˆ โ„ค))
60 eluzelre 12829 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„)
61 2z 12590 . . . . . . . . . . . . . . . . . . . . . . . 24 2 โˆˆ โ„ค
6261eluz1i 12826 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†” (๐‘ฅ โˆˆ โ„ค โˆง 2 โ‰ค ๐‘ฅ))
63 2pos 12311 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 < 2
64 zre 12558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„)
65 0re 11212 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 โˆˆ โ„
66 2re 12282 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2 โˆˆ โ„
67 ltletr 11302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((0 โˆˆ โ„ โˆง 2 โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„) โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
6865, 66, 67mp3an12 1451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฅ โˆˆ โ„ โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
6964, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฅ โˆˆ โ„ค โ†’ ((0 < 2 โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ))
7063, 69mpani 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฅ โˆˆ โ„ค โ†’ (2 โ‰ค ๐‘ฅ โ†’ 0 < ๐‘ฅ))
7170imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ฅ โˆˆ โ„ค โˆง 2 โ‰ค ๐‘ฅ) โ†’ 0 < ๐‘ฅ)
7262, 71sylbi 216 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ 0 < ๐‘ฅ)
7360, 72jca 512 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ))
74 divgt0 12078 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ) โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ 0 < (๐‘ฅ / ๐‘ž))
7573, 45, 74syl2anr 597 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ 0 < (๐‘ฅ / ๐‘ž))
7675a1d 25 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ 0 < (๐‘ฅ / ๐‘ž)))
7776ancld 551 . . . . . . . . . . . . . . . . . 18 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ฅ / ๐‘ž))))
78 elnnz 12564 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†” ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง 0 < (๐‘ฅ / ๐‘ž)))
7977, 78syl6ibr 251 . . . . . . . . . . . . . . . . 17 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„ค โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
8059, 79sylbid 239 . . . . . . . . . . . . . . . 16 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
8180ancoms 459 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„•))
82 breq1 5150 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (๐‘ฆ < ๐‘ฅ โ†” (๐‘ฅ / ๐‘ž) < ๐‘ฅ))
83 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (๐‘˜ < ๐‘ฆ โ†” ๐‘˜ < (๐‘ฅ / ๐‘ž)))
84 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
8584bibi2d 342 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
8685notbid 317 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
87862rexbidv 3219 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
8883, 87imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)) โ†” (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
8988ralbidv 3177 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
9082, 89imbi12d 344 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฆ = (๐‘ฅ / ๐‘ž) โ†’ ((๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†” ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
9190rspcv 3608 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
92913ad2ant1 1133 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
9392adantl 482 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
94 eluzelcn 12830 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„‚)
9594mullidd 11228 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
9695ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 ยท ๐‘ฅ) = ๐‘ฅ)
97 prmgt1 16630 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ž โˆˆ โ„™ โ†’ 1 < ๐‘ž)
9897ad2antlr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 1 < ๐‘ž)
99 1red 11211 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 1 โˆˆ โ„)
10028nnred 12223 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„)
101100ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„)
10260ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ฅ โˆˆ โ„)
10372ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 0 < ๐‘ฅ)
104 ltmul1 12060 . . . . . . . . . . . . . . . . . . . . . 22 ((1 โˆˆ โ„ โˆง ๐‘ž โˆˆ โ„ โˆง (๐‘ฅ โˆˆ โ„ โˆง 0 < ๐‘ฅ)) โ†’ (1 < ๐‘ž โ†” (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ)))
10599, 101, 102, 103, 104syl112anc 1374 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 < ๐‘ž โ†” (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ)))
10698, 105mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (1 ยท ๐‘ฅ) < (๐‘ž ยท ๐‘ฅ))
10796, 106eqbrtrrd 5171 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ฅ < (๐‘ž ยท ๐‘ฅ))
10828, 43syl 17 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ž โˆˆ โ„™ โ†’ 0 < ๐‘ž)
109108ad2antlr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ 0 < ๐‘ž)
110 ltdivmul 12085 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„ โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†” ๐‘ฅ < (๐‘ž ยท ๐‘ฅ)))
111102, 102, 101, 109, 110syl112anc 1374 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†” ๐‘ฅ < (๐‘ž ยท ๐‘ฅ)))
112107, 111mpbird 256 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ฅ / ๐‘ž) < ๐‘ฅ)
113 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
114 breq2 5151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
115114bibi1d 343 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
116115notbid 317 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
1171162rexbidv 3219 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
118113, 117imbi12d 344 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘˜ = (๐‘ก / ๐‘ž) โ†’ ((๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†” ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
119118rspcv 3608 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
1201193ad2ant2 1134 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
121120adantl 482 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
122393ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„)
123122adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ ๐‘ก โˆˆ โ„)
124 ltdiv1 12074 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ก โˆˆ โ„ โˆง ๐‘ฅ โˆˆ โ„ โˆง (๐‘ž โˆˆ โ„ โˆง 0 < ๐‘ž)) โ†’ (๐‘ก < ๐‘ฅ โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
125123, 102, 101, 109, 124syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†” (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž)))
126125biimpa 477 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž))
127 simprll 777 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ ๐‘ โˆˆ โ„™)
128 peano2nn 12220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘› โˆˆ โ„• โ†’ (๐‘› + 1) โˆˆ โ„•)
129128adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘› + 1) โˆˆ โ„•)
130129ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘› + 1) โˆˆ โ„•)
13126ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„ค)
132 nnnn0 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (๐‘› โˆˆ โ„• โ†’ ๐‘› โˆˆ โ„•0)
133132ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘› โˆˆ โ„•0)
134 zexpcl 14038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((๐‘ž โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•0) โ†’ (๐‘žโ†‘๐‘›) โˆˆ โ„ค)
135131, 133, 134syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘žโ†‘๐‘›) โˆˆ โ„ค)
136 nnz 12575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
1371363ad2ant2 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
138137ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
13929ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โ‰  0)
140 dvdsmulcr 16225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐‘žโ†‘๐‘›) โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค โˆง (๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
141135, 138, 131, 139, 140syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
14228nncnd 12224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (๐‘ž โˆˆ โ„™ โ†’ ๐‘ž โˆˆ โ„‚)
143142ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„‚)
144143, 133expp1d 14108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘žโ†‘(๐‘› + 1)) = ((๐‘žโ†‘๐‘›) ยท ๐‘ž))
145144eqcomd 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) ยท ๐‘ž) = (๐‘žโ†‘(๐‘› + 1)))
146 nncn 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (๐‘ก โˆˆ โ„• โ†’ ๐‘ก โˆˆ โ„‚)
1471463ad2ant3 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ ๐‘ก โˆˆ โ„‚)
148147ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ก โˆˆ โ„‚)
149148, 143, 139divcan1d 11987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) ยท ๐‘ž) = ๐‘ก)
150145, 149breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ก / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
151141, 150bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
152 nnz 12575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
1531523ad2ant1 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
154153ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
155 dvdsmulcr 16225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((๐‘žโ†‘๐‘›) โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค โˆง (๐‘ž โˆˆ โ„ค โˆง ๐‘ž โ‰  0)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
156135, 154, 131, 139, 155syl112anc 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
15794ad4antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ฅ โˆˆ โ„‚)
158157, 143, 139divcan1d 11987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) = ๐‘ฅ)
159145, 158breq12d 5160 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) ยท ๐‘ž) โˆฅ ((๐‘ฅ / ๐‘ž) ยท ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
160156, 159bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
161151, 160bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
162161notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
163162biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
164163impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
165 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘š = (๐‘› + 1) โ†’ (๐‘žโ†‘๐‘š) = (๐‘žโ†‘(๐‘› + 1)))
166165breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = (๐‘› + 1) โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก))
167165breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = (๐‘› + 1) โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ))
168166, 167bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘š = (๐‘› + 1) โ†’ (((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
169168notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘š = (๐‘› + 1) โ†’ (ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)))
170169rspcev 3612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((๐‘› + 1) โˆˆ โ„• โˆง ยฌ ((๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ก โ†” (๐‘žโ†‘(๐‘› + 1)) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
171130, 164, 170syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
172 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘๐‘›) = (๐‘žโ†‘๐‘›))
173172breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
174172breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
175173, 174bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
176175notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))
177176anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ = ๐‘ž โ†’ (((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†” ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))))
178177anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ = ๐‘ž โ†’ (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†” ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))))))
179 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘ = ๐‘ž โ†’ (๐‘โ†‘๐‘š) = (๐‘žโ†‘๐‘š))
180179breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ก))
181179breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ = ๐‘ž โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
182180, 181bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ = ๐‘ž โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
183182notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
184183rexbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ = ๐‘ž โ†’ (โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
185178, 184imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ = ๐‘ž โ†’ ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘žโ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘žโ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))))
186171, 185mpbiri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ = ๐‘ž โ†’ (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
187186com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
188 simplr 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž) โ†’ ๐‘› โˆˆ โ„•)
189188ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ๐‘› โˆˆ โ„•)
190 prmz 16608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (๐‘ โˆˆ โ„™ โ†’ ๐‘ โˆˆ โ„ค)
191190adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘ โˆˆ โ„ค)
192191ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ โˆˆ โ„ค)
193132adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ ๐‘› โˆˆ โ„•0)
194193ad2antrl 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘› โˆˆ โ„•0)
195 zexpcl 14038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((๐‘ โˆˆ โ„ค โˆง ๐‘› โˆˆ โ„•0) โ†’ (๐‘โ†‘๐‘›) โˆˆ โ„ค)
196192, 194, 195syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆˆ โ„ค)
19726ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„ค)
198137ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ก / ๐‘ž) โˆˆ โ„ค)
199 dvdsmultr2 16237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
200196, 197, 198, 199syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
201196, 197gcdcomd 16451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) gcd ๐‘ž) = (๐‘ž gcd (๐‘โ†‘๐‘›)))
202 simp-4r 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ž โˆˆ โ„™)
203 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘ โˆˆ โ„™)
204 simprr 771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ ๐‘› โˆˆ โ„•)
205 prmdvdsexpb 16649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” ๐‘ž = ๐‘))
206 equcom 2021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (๐‘ž = ๐‘ โ†” ๐‘ = ๐‘ž)
207205, 206bitrdi 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” ๐‘ = ๐‘ž))
208207biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†’ ๐‘ = ๐‘ž))
209202, 203, 204, 208syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†’ ๐‘ = ๐‘ž))
210209con3d 152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›)))
211210impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›))
212 simp-4r 782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„™)
213 coprm 16644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((๐‘ž โˆˆ โ„™ โˆง (๐‘โ†‘๐‘›) โˆˆ โ„ค) โ†’ (ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1))
214212, 196, 213syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ๐‘ž โˆฅ (๐‘โ†‘๐‘›) โ†” (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1))
215211, 214mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž gcd (๐‘โ†‘๐‘›)) = 1)
216201, 215eqtrd 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1)
217 coprmdvds 16586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ก / ๐‘ž) โˆˆ โ„ค) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
218196, 197, 198, 217syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
219216, 218mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž)))
220200, 219impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž))))
221147ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ก โˆˆ โ„‚)
222142ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โˆˆ โ„‚)
22329ad4antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ž โ‰  0)
224221, 222, 223divcan2d 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž ยท (๐‘ก / ๐‘ž)) = ๐‘ก)
225224breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ก / ๐‘ž)) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
226220, 225bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
227153ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ฅ / ๐‘ž) โˆˆ โ„ค)
228 dvdsmultr2 16237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
229196, 197, 227, 228syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
230 coprmdvds 16586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((๐‘โ†‘๐‘›) โˆˆ โ„ค โˆง ๐‘ž โˆˆ โ„ค โˆง (๐‘ฅ / ๐‘ž) โˆˆ โ„ค) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
231196, 197, 227, 230syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โˆง ((๐‘โ†‘๐‘›) gcd ๐‘ž) = 1) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
232216, 231mpan2d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โ†’ (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))
233229, 232impbid 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž))))
23494ad4antr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ๐‘ฅ โˆˆ โ„‚)
235234, 222, 223divcan2d 11988 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) = ๐‘ฅ)
236235breq2d 5159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ž ยท (๐‘ฅ / ๐‘ž)) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
237233, 236bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
238226, 237bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
239238notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
240239biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
241 oveq2 7413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (๐‘š = ๐‘› โ†’ (๐‘โ†‘๐‘š) = (๐‘โ†‘๐‘›))
242241breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ก))
243241breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
244242, 243bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (๐‘š = ๐‘› โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
245244notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘š = ๐‘› โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
246245rspcev 3612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐‘› โˆˆ โ„• โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
247189, 240, 246syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
248247ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ๐‘ = ๐‘ž)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
249248expr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))))
250249com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง (๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•)) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))))
251250impr 455 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (ยฌ ๐‘ = ๐‘ž โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
252187, 251pm2.61d 179 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
253 oveq1 7412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘Ÿ = ๐‘ โ†’ (๐‘Ÿโ†‘๐‘š) = (๐‘โ†‘๐‘š))
254253breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ก))
255253breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ))
256254, 255bibi12d 345 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘Ÿ = ๐‘ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
257256notbid 317 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘Ÿ = ๐‘ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
258257rexbidv 3178 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘Ÿ = ๐‘ โ†’ (โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
259258rspcev 3612 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ โˆˆ โ„™ โˆง โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
260127, 252, 259syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โˆง ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โˆง ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
261260exp32 421 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ ((๐‘ โˆˆ โ„™ โˆง ๐‘› โˆˆ โ„•) โ†’ (ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
262261rexlimdvv 3210 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
263126, 262embantd 59 . . . . . . . . . . . . . . . . . . . . 21 ((((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โˆง ๐‘ก < ๐‘ฅ) โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
264263ex 413 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
265264com23 86 . . . . . . . . . . . . . . . . . . 19 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (((๐‘ก / ๐‘ž) < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ (๐‘ก / ๐‘ž) โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
266121, 265syld 47 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
267112, 266embantd 59 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (((๐‘ฅ / ๐‘ž) < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < (๐‘ฅ / ๐‘ž) โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ (๐‘ฅ / ๐‘ž)))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
26893, 267syld 47 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โˆง ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โˆง (๐‘ก / ๐‘ž) โˆˆ โ„• โˆง ๐‘ก โˆˆ โ„•)) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
2692683exp2 1354 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ ((๐‘ฅ / ๐‘ž) โˆˆ โ„• โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))))))
27081, 269syld 47 . . . . . . . . . . . . . 14 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™) โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))))))
2712703impia 1117 . . . . . . . . . . . . 13 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก โˆˆ โ„• โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))))
272271com24 95 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ (๐‘ก โˆˆ โ„• โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))))
273272imp32 419 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ ((๐‘ก / ๐‘ž) โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
27437, 53, 2733syld 60 . . . . . . . . . 10 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
275 simpl2 1192 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ๐‘ž โˆˆ โ„™)
276 1nn 12219 . . . . . . . . . . . . . . 15 1 โˆˆ โ„•
277276a1i 11 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ 1 โˆˆ โ„•)
278142exp1d 14102 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ž โˆˆ โ„™ โ†’ (๐‘žโ†‘1) = ๐‘ž)
279278breq1d 5157 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ž โˆˆ โ„™ โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” ๐‘ž โˆฅ ๐‘ก))
280279notbid 317 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ โ„™ โ†’ (ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก โ†” ยฌ ๐‘ž โˆฅ ๐‘ก))
281280biimpar 478 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ยฌ ๐‘ž โˆฅ ๐‘ก) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
2822813ad2antl2 1186 . . . . . . . . . . . . . . . . . 18 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ยฌ ๐‘ž โˆฅ ๐‘ก) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
283282adantrr 715 . . . . . . . . . . . . . . . . 17 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ)) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
284283adantrl 714 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ ยฌ (๐‘žโ†‘1) โˆฅ ๐‘ก)
285278breq1d 5157 . . . . . . . . . . . . . . . . . . . 20 (๐‘ž โˆˆ โ„™ โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†” ๐‘ž โˆฅ ๐‘ฅ))
286285biimpar 478 . . . . . . . . . . . . . . . . . . 19 ((๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ฅ)
2872863adant1 1130 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ฅ)
288 idd 24 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก) โ†’ ((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก)))
289287, 288mpid 44 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โ†’ (((๐‘žโ†‘1) โˆฅ ๐‘ฅ โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก) โ†’ (๐‘žโ†‘1) โˆฅ ๐‘ก))
290289adantr 481 . . . . . . . . . . . . . . . 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 5157 . . . . . . . . . . . . . . . . 17 (๐‘Ÿ = ๐‘ž โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ก))
296294breq1d 5157 . . . . . . . . . . . . . . . . 17 (๐‘Ÿ = ๐‘ž โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ))
297295, 296bibi12d 345 . . . . . . . . . . . . . . . 16 (๐‘Ÿ = ๐‘ž โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
298297notbid 317 . . . . . . . . . . . . . . 15 (๐‘Ÿ = ๐‘ž โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ)))
299 oveq2 7413 . . . . . . . . . . . . . . . . . 18 (๐‘š = 1 โ†’ (๐‘žโ†‘๐‘š) = (๐‘žโ†‘1))
300299breq1d 5157 . . . . . . . . . . . . . . . . 17 (๐‘š = 1 โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ก))
301299breq1d 5157 . . . . . . . . . . . . . . . . 17 (๐‘š = 1 โ†’ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ))
302300, 301bibi12d 345 . . . . . . . . . . . . . . . 16 (๐‘š = 1 โ†’ (((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)))
303302notbid 317 . . . . . . . . . . . . . . 15 (๐‘š = 1 โ†’ (ยฌ ((๐‘žโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘žโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)))
304298, 303rspc2ev 3623 . . . . . . . . . . . . . 14 ((๐‘ž โˆˆ โ„™ โˆง 1 โˆˆ โ„• โˆง ยฌ ((๐‘žโ†‘1) โˆฅ ๐‘ก โ†” (๐‘žโ†‘1) โˆฅ ๐‘ฅ)) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
305275, 277, 293, 304syl3anc 1371 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (๐‘ก โˆˆ โ„• โˆง (ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ))) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))
306305expr 457 . . . . . . . . . . . 12 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ ((ยฌ ๐‘ž โˆฅ ๐‘ก โˆง ๐‘ก < ๐‘ฅ) โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
307306expd 416 . . . . . . . . . . 11 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง ๐‘ก โˆˆ โ„•) โ†’ (ยฌ ๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
308307adantrl 714 . . . . . . . . . 10 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (ยฌ ๐‘ž โˆฅ ๐‘ก โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
309274, 308pm2.61d 179 . . . . . . . . 9 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โˆง ๐‘ก โˆˆ โ„•)) โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
310309expr 457 . . . . . . . 8 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ (๐‘ก โˆˆ โ„• โ†’ (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ))))
311310ralrimiv 3145 . . . . . . 7 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ โˆ€๐‘ก โˆˆ โ„• (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
312 breq1 5150 . . . . . . . . 9 (๐‘ก = ๐‘˜ โ†’ (๐‘ก < ๐‘ฅ โ†” ๐‘˜ < ๐‘ฅ))
313 breq2 5151 . . . . . . . . . . . . 13 (๐‘ก = ๐‘˜ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜))
314313bibi1d 343 . . . . . . . . . . . 12 (๐‘ก = ๐‘˜ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
315314notbid 317 . . . . . . . . . . 11 (๐‘ก = ๐‘˜ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
3163152rexbidv 3219 . . . . . . . . . 10 (๐‘ก = ๐‘˜ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)))
317253breq1d 5157 . . . . . . . . . . . . 13 (๐‘Ÿ = ๐‘ โ†’ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘˜))
318317, 255bibi12d 345 . . . . . . . . . . . 12 (๐‘Ÿ = ๐‘ โ†’ (((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
319318notbid 317 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ โ†’ (ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ)))
320241breq1d 5157 . . . . . . . . . . . . 13 (๐‘š = ๐‘› โ†’ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘˜))
321320, 243bibi12d 345 . . . . . . . . . . . 12 (๐‘š = ๐‘› โ†’ (((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
322321notbid 317 . . . . . . . . . . 11 (๐‘š = ๐‘› โ†’ (ยฌ ((๐‘โ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
323319, 322cbvrex2vw 3239 . . . . . . . . . 10 (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘˜ โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))
324316, 323bitrdi 286 . . . . . . . . 9 (๐‘ก = ๐‘˜ โ†’ (โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ) โ†” โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
325312, 324imbi12d 344 . . . . . . . 8 (๐‘ก = ๐‘˜ โ†’ ((๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))
326325cbvralvw 3234 . . . . . . 7 (โˆ€๐‘ก โˆˆ โ„• (๐‘ก < ๐‘ฅ โ†’ โˆƒ๐‘Ÿ โˆˆ โ„™ โˆƒ๐‘š โˆˆ โ„• ยฌ ((๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ก โ†” (๐‘Ÿโ†‘๐‘š) โˆฅ ๐‘ฅ)) โ†” โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
327311, 326sylib 217 . . . . . 6 (((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ž โˆˆ โ„™ โˆง ๐‘ž โˆฅ ๐‘ฅ) โˆง โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ)))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
3283273exp1 1352 . . . . 5 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (๐‘ž โˆˆ โ„™ โ†’ (๐‘ž โˆฅ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))))
329328rexlimdv 3153 . . . 4 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (โˆƒ๐‘ž โˆˆ โ„™ ๐‘ž โˆฅ ๐‘ฅ โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))))
33025, 329mpd 15 . . 3 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ (โˆ€๐‘ฆ โˆˆ โ„• (๐‘ฆ < ๐‘ฅ โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฆ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฆ))) โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ))))
33114, 21, 24, 330indstr2 12907 . 2 (๐‘ฅ โˆˆ โ„• โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐‘ฅ โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐‘ฅ)))
3327, 331vtoclga 3565 1 (๐ด โˆˆ โ„• โ†’ โˆ€๐‘˜ โˆˆ โ„• (๐‘˜ < ๐ด โ†’ โˆƒ๐‘ โˆˆ โ„™ โˆƒ๐‘› โˆˆ โ„• ยฌ ((๐‘โ†‘๐‘›) โˆฅ ๐‘˜ โ†” (๐‘โ†‘๐‘›) โˆฅ ๐ด)))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070   class class class wbr 5147  โ€˜cfv 6540  (class class class)co 7405  โ„‚cc 11104  โ„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   ยท cmul 11111   < clt 11244   โ‰ค cle 11245   / cdiv 11867  โ„•cn 12208  2c2 12263  โ„•0cn0 12468  โ„คcz 12554  โ„คโ‰ฅcuz 12818  โ†‘cexp 14023   โˆฅ cdvds 16193   gcd cgcd 16431  โ„™cprime 16604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-rp 12971  df-fz 13481  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-dvds 16194  df-gcd 16432  df-prm 16605
This theorem is referenced by:  nn0prpw  35196
  Copyright terms: Public domain W3C validator