MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ply1divex Structured version   Visualization version   GIF version

Theorem ply1divex 25524
Description: Lemma for ply1divalg 25525: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.)
Hypotheses
Ref Expression
ply1divalg.p ๐‘ƒ = (Poly1โ€˜๐‘…)
ply1divalg.d ๐ท = ( deg1 โ€˜๐‘…)
ply1divalg.b ๐ต = (Baseโ€˜๐‘ƒ)
ply1divalg.m โˆ’ = (-gโ€˜๐‘ƒ)
ply1divalg.z 0 = (0gโ€˜๐‘ƒ)
ply1divalg.t โˆ™ = (.rโ€˜๐‘ƒ)
ply1divalg.r1 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
ply1divalg.f (๐œ‘ โ†’ ๐น โˆˆ ๐ต)
ply1divalg.g1 (๐œ‘ โ†’ ๐บ โˆˆ ๐ต)
ply1divalg.g2 (๐œ‘ โ†’ ๐บ โ‰  0 )
ply1divex.o 1 = (1rโ€˜๐‘…)
ply1divex.k ๐พ = (Baseโ€˜๐‘…)
ply1divex.u ยท = (.rโ€˜๐‘…)
ply1divex.i (๐œ‘ โ†’ ๐ผ โˆˆ ๐พ)
ply1divex.g3 (๐œ‘ โ†’ (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) = 1 )
Assertion
Ref Expression
ply1divex (๐œ‘ โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
Distinct variable groups:   0 ,๐‘ž   ๐น,๐‘ž   ๐ผ,๐‘ž   ๐‘ƒ,๐‘ž   ๐‘…,๐‘ž   โˆ’ ,๐‘ž   ๐ต,๐‘ž   โˆ™ ,๐‘ž   ๐ท,๐‘ž   ๐บ,๐‘ž   ๐œ‘,๐‘ž   ยท ,๐‘ž
Allowed substitution hints:   1 (๐‘ž)   ๐พ(๐‘ž)

Proof of Theorem ply1divex
Dummy variables ๐‘‘ ๐‘“ ๐‘Ÿ ๐‘Ž ๐‘” are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6846 . . . . 5 (๐น = 0 โ†’ (๐ทโ€˜๐น) = (๐ทโ€˜ 0 ))
21breq1d 5119 . . . 4 (๐น = 0 โ†’ ((๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†” (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + ๐‘‘)))
32rexbidv 3172 . . 3 (๐น = 0 โ†’ (โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†” โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + ๐‘‘)))
4 nnssnn0 12424 . . . . 5 โ„• โŠ† โ„•0
5 ply1divalg.r1 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘… โˆˆ Ring)
65adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ ๐‘… โˆˆ Ring)
7 ply1divalg.f . . . . . . . . . 10 (๐œ‘ โ†’ ๐น โˆˆ ๐ต)
87adantr 482 . . . . . . . . 9 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ ๐น โˆˆ ๐ต)
9 simpr 486 . . . . . . . . 9 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ ๐น โ‰  0 )
10 ply1divalg.d . . . . . . . . . 10 ๐ท = ( deg1 โ€˜๐‘…)
11 ply1divalg.p . . . . . . . . . 10 ๐‘ƒ = (Poly1โ€˜๐‘…)
12 ply1divalg.z . . . . . . . . . 10 0 = (0gโ€˜๐‘ƒ)
13 ply1divalg.b . . . . . . . . . 10 ๐ต = (Baseโ€˜๐‘ƒ)
1410, 11, 12, 13deg1nn0cl 25476 . . . . . . . . 9 ((๐‘… โˆˆ Ring โˆง ๐น โˆˆ ๐ต โˆง ๐น โ‰  0 ) โ†’ (๐ทโ€˜๐น) โˆˆ โ„•0)
156, 8, 9, 14syl3anc 1372 . . . . . . . 8 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ (๐ทโ€˜๐น) โˆˆ โ„•0)
1615nn0red 12482 . . . . . . 7 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ (๐ทโ€˜๐น) โˆˆ โ„)
17 ply1divalg.g1 . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ โˆˆ ๐ต)
18 ply1divalg.g2 . . . . . . . . . 10 (๐œ‘ โ†’ ๐บ โ‰  0 )
1910, 11, 12, 13deg1nn0cl 25476 . . . . . . . . . 10 ((๐‘… โˆˆ Ring โˆง ๐บ โˆˆ ๐ต โˆง ๐บ โ‰  0 ) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„•0)
205, 17, 18, 19syl3anc 1372 . . . . . . . . 9 (๐œ‘ โ†’ (๐ทโ€˜๐บ) โˆˆ โ„•0)
2120nn0red 12482 . . . . . . . 8 (๐œ‘ โ†’ (๐ทโ€˜๐บ) โˆˆ โ„)
2221adantr 482 . . . . . . 7 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„)
2316, 22resubcld 11591 . . . . . 6 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) โˆˆ โ„)
24 arch 12418 . . . . . 6 (((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) โˆˆ โ„ โ†’ โˆƒ๐‘‘ โˆˆ โ„• ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘)
2523, 24syl 17 . . . . 5 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ โˆƒ๐‘‘ โˆˆ โ„• ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘)
26 ssrexv 4015 . . . . 5 (โ„• โŠ† โ„•0 โ†’ (โˆƒ๐‘‘ โˆˆ โ„• ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘ โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘))
274, 25, 26mpsyl 68 . . . 4 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘)
2816adantr 482 . . . . . . 7 (((๐œ‘ โˆง ๐น โ‰  0 ) โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐ทโ€˜๐น) โˆˆ โ„)
2921ad2antrr 725 . . . . . . 7 (((๐œ‘ โˆง ๐น โ‰  0 ) โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„)
30 nn0re 12430 . . . . . . . 8 (๐‘‘ โˆˆ โ„•0 โ†’ ๐‘‘ โˆˆ โ„)
3130adantl 483 . . . . . . 7 (((๐œ‘ โˆง ๐น โ‰  0 ) โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ๐‘‘ โˆˆ โ„)
3228, 29, 31ltsubadd2d 11761 . . . . . 6 (((๐œ‘ โˆง ๐น โ‰  0 ) โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘ โ†” (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘)))
3332biimpd 228 . . . . 5 (((๐œ‘ โˆง ๐น โ‰  0 ) โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘ โ†’ (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘)))
3433reximdva 3162 . . . 4 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ (โˆƒ๐‘‘ โˆˆ โ„•0 ((๐ทโ€˜๐น) โˆ’ (๐ทโ€˜๐บ)) < ๐‘‘ โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘)))
3527, 34mpd 15 . . 3 ((๐œ‘ โˆง ๐น โ‰  0 ) โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘))
36 0nn0 12436 . . . 4 0 โˆˆ โ„•0
3710, 11, 12deg1z 25475 . . . . . 6 (๐‘… โˆˆ Ring โ†’ (๐ทโ€˜ 0 ) = -โˆž)
385, 37syl 17 . . . . 5 (๐œ‘ โ†’ (๐ทโ€˜ 0 ) = -โˆž)
39 0re 11165 . . . . . . 7 0 โˆˆ โ„
40 readdcl 11142 . . . . . . 7 (((๐ทโ€˜๐บ) โˆˆ โ„ โˆง 0 โˆˆ โ„) โ†’ ((๐ทโ€˜๐บ) + 0) โˆˆ โ„)
4121, 39, 40sylancl 587 . . . . . 6 (๐œ‘ โ†’ ((๐ทโ€˜๐บ) + 0) โˆˆ โ„)
4241mnfltd 13053 . . . . 5 (๐œ‘ โ†’ -โˆž < ((๐ทโ€˜๐บ) + 0))
4338, 42eqbrtrd 5131 . . . 4 (๐œ‘ โ†’ (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + 0))
44 oveq2 7369 . . . . . 6 (๐‘‘ = 0 โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) = ((๐ทโ€˜๐บ) + 0))
4544breq2d 5121 . . . . 5 (๐‘‘ = 0 โ†’ ((๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†” (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + 0)))
4645rspcev 3583 . . . 4 ((0 โˆˆ โ„•0 โˆง (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + 0)) โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + ๐‘‘))
4736, 43, 46sylancr 588 . . 3 (๐œ‘ โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜ 0 ) < ((๐ทโ€˜๐บ) + ๐‘‘))
483, 35, 47pm2.61ne 3027 . 2 (๐œ‘ โ†’ โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘))
49 fveq2 6846 . . . . . 6 (๐‘“ = ๐น โ†’ (๐ทโ€˜๐‘“) = (๐ทโ€˜๐น))
5049breq1d 5119 . . . . 5 (๐‘“ = ๐น โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†” (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘)))
51 fvoveq1 7384 . . . . . . 7 (๐‘“ = ๐น โ†’ (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) = (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))))
5251breq1d 5119 . . . . . 6 (๐‘“ = ๐น โ†’ ((๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
5352rexbidv 3172 . . . . 5 (๐‘“ = ๐น โ†’ (โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
5450, 53imbi12d 345 . . . 4 (๐‘“ = ๐น โ†’ (((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
55 oveq2 7369 . . . . . . . . . 10 (๐‘Ž = 0 โ†’ ((๐ทโ€˜๐บ) + ๐‘Ž) = ((๐ทโ€˜๐บ) + 0))
5655breq2d 5121 . . . . . . . . 9 (๐‘Ž = 0 โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†” (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0)))
5756imbi1d 342 . . . . . . . 8 (๐‘Ž = 0 โ†’ (((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
5857ralbidv 3171 . . . . . . 7 (๐‘Ž = 0 โ†’ (โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
5958imbi2d 341 . . . . . 6 (๐‘Ž = 0 โ†’ ((๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))) โ†” (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
60 oveq2 7369 . . . . . . . . . 10 (๐‘Ž = ๐‘‘ โ†’ ((๐ทโ€˜๐บ) + ๐‘Ž) = ((๐ทโ€˜๐บ) + ๐‘‘))
6160breq2d 5121 . . . . . . . . 9 (๐‘Ž = ๐‘‘ โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†” (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘)))
6261imbi1d 342 . . . . . . . 8 (๐‘Ž = ๐‘‘ โ†’ (((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
6362ralbidv 3171 . . . . . . 7 (๐‘Ž = ๐‘‘ โ†’ (โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
6463imbi2d 341 . . . . . 6 (๐‘Ž = ๐‘‘ โ†’ ((๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))) โ†” (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
65 oveq2 7369 . . . . . . . . . 10 (๐‘Ž = (๐‘‘ + 1) โ†’ ((๐ทโ€˜๐บ) + ๐‘Ž) = ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))
6665breq2d 5121 . . . . . . . . 9 (๐‘Ž = (๐‘‘ + 1) โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†” (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1))))
6766imbi1d 342 . . . . . . . 8 (๐‘Ž = (๐‘‘ + 1) โ†’ (((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
6867ralbidv 3171 . . . . . . 7 (๐‘Ž = (๐‘‘ + 1) โ†’ (โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
6968imbi2d 341 . . . . . 6 (๐‘Ž = (๐‘‘ + 1) โ†’ ((๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘Ž) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))) โ†” (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
7011ply1ring 21642 . . . . . . . . . . . 12 (๐‘… โˆˆ Ring โ†’ ๐‘ƒ โˆˆ Ring)
715, 70syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ƒ โˆˆ Ring)
7213, 12ring0cl 19998 . . . . . . . . . . 11 (๐‘ƒ โˆˆ Ring โ†’ 0 โˆˆ ๐ต)
7371, 72syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โˆˆ ๐ต)
7473ad2antrr 725 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โˆง (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0)) โ†’ 0 โˆˆ ๐ต)
75 ply1divalg.t . . . . . . . . . . . . . . . . 17 โˆ™ = (.rโ€˜๐‘ƒ)
7613, 75, 12ringrz 20020 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ Ring โˆง ๐บ โˆˆ ๐ต) โ†’ (๐บ โˆ™ 0 ) = 0 )
7771, 17, 76syl2anc 585 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐บ โˆ™ 0 ) = 0 )
7877oveq2d 7377 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘“ โˆ’ (๐บ โˆ™ 0 )) = (๐‘“ โˆ’ 0 ))
7978adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ (๐‘“ โˆ’ (๐บ โˆ™ 0 )) = (๐‘“ โˆ’ 0 ))
80 ringgrp 19977 . . . . . . . . . . . . . . 15 (๐‘ƒ โˆˆ Ring โ†’ ๐‘ƒ โˆˆ Grp)
8171, 80syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘ƒ โˆˆ Grp)
82 ply1divalg.m . . . . . . . . . . . . . . 15 โˆ’ = (-gโ€˜๐‘ƒ)
8313, 12, 82grpsubid1 18840 . . . . . . . . . . . . . 14 ((๐‘ƒ โˆˆ Grp โˆง ๐‘“ โˆˆ ๐ต) โ†’ (๐‘“ โˆ’ 0 ) = ๐‘“)
8481, 83sylan 581 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ (๐‘“ โˆ’ 0 ) = ๐‘“)
8579, 84eqtr2d 2774 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ ๐‘“ = (๐‘“ โˆ’ (๐บ โˆ™ 0 )))
8685fveq2d 6850 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ (๐ทโ€˜๐‘“) = (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))))
8720nn0cnd 12483 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ทโ€˜๐บ) โˆˆ โ„‚)
8887addid1d 11363 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ทโ€˜๐บ) + 0) = (๐ทโ€˜๐บ))
8988adantr 482 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐บ) + 0) = (๐ทโ€˜๐บ))
9086, 89breq12d 5122 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†” (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))) < (๐ทโ€˜๐บ)))
9190biimpa 478 . . . . . . . . 9 (((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โˆง (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0)) โ†’ (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))) < (๐ทโ€˜๐บ))
92 oveq2 7369 . . . . . . . . . . . . 13 (๐‘ž = 0 โ†’ (๐บ โˆ™ ๐‘ž) = (๐บ โˆ™ 0 ))
9392oveq2d 7377 . . . . . . . . . . . 12 (๐‘ž = 0 โ†’ (๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž)) = (๐‘“ โˆ’ (๐บ โˆ™ 0 )))
9493fveq2d 6850 . . . . . . . . . . 11 (๐‘ž = 0 โ†’ (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) = (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))))
9594breq1d 5119 . . . . . . . . . 10 (๐‘ž = 0 โ†’ ((๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))) < (๐ทโ€˜๐บ)))
9695rspcev 3583 . . . . . . . . 9 (( 0 โˆˆ ๐ต โˆง (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ 0 ))) < (๐ทโ€˜๐บ)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
9774, 91, 96syl2anc 585 . . . . . . . 8 (((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โˆง (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
9897ex 414 . . . . . . 7 ((๐œ‘ โˆง ๐‘“ โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
9998ralrimiva 3140 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + 0) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
100 nn0addcl 12456 . . . . . . . . . . . . . . . . . 18 (((๐ทโ€˜๐บ) โˆˆ โ„•0 โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) โˆˆ โ„•0)
10120, 100sylan 581 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) โˆˆ โ„•0)
102101adantr 482 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) โˆˆ โ„•0)
1035ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ ๐‘… โˆˆ Ring)
104 simprl 770 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ ๐‘” โˆˆ ๐ต)
10510, 11, 13deg1cl 25471 . . . . . . . . . . . . . . . . . . . 20 (๐‘” โˆˆ ๐ต โ†’ (๐ทโ€˜๐‘”) โˆˆ (โ„•0 โˆช {-โˆž}))
10620ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„•0)
107 peano2nn0 12461 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘‘ โˆˆ โ„•0 โ†’ (๐‘‘ + 1) โˆˆ โ„•0)
108107ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐‘‘ + 1) โˆˆ โ„•0)
109106, 108nn0addcld 12485 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆˆ โ„•0)
110109nn0zd 12533 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆˆ โ„ค)
111 degltlem1 25460 . . . . . . . . . . . . . . . . . . . 20 (((๐ทโ€˜๐‘”) โˆˆ (โ„•0 โˆช {-โˆž}) โˆง ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆˆ โ„ค) โ†’ ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†” (๐ทโ€˜๐‘”) โ‰ค (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1)))
112105, 110, 111syl2an2 685 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†” (๐ทโ€˜๐‘”) โ‰ค (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1)))
113112biimpd 228 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ (๐ทโ€˜๐‘”) โ‰ค (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1)))
114113impr 456 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐ทโ€˜๐‘”) โ‰ค (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1))
11520adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„•0)
116115nn0cnd 12483 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„‚)
117 nn0cn 12431 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘‘ โˆˆ โ„•0 โ†’ ๐‘‘ โˆˆ โ„‚)
118117adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ๐‘‘ โˆˆ โ„‚)
119 peano2cn 11335 . . . . . . . . . . . . . . . . . . . . 21 (๐‘‘ โˆˆ โ„‚ โ†’ (๐‘‘ + 1) โˆˆ โ„‚)
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐‘‘ + 1) โˆˆ โ„‚)
121 1cnd 11158 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ 1 โˆˆ โ„‚)
122116, 120, 121addsubassd 11540 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1) = ((๐ทโ€˜๐บ) + ((๐‘‘ + 1) โˆ’ 1)))
123 ax-1cn 11117 . . . . . . . . . . . . . . . . . . . . 21 1 โˆˆ โ„‚
124 pncan 11415 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘‘ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘‘ + 1) โˆ’ 1) = ๐‘‘)
125118, 123, 124sylancl 587 . . . . . . . . . . . . . . . . . . . 20 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐‘‘ + 1) โˆ’ 1) = ๐‘‘)
126125oveq2d 7377 . . . . . . . . . . . . . . . . . . 19 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐ทโ€˜๐บ) + ((๐‘‘ + 1) โˆ’ 1)) = ((๐ทโ€˜๐บ) + ๐‘‘))
127122, 126eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1) = ((๐ทโ€˜๐บ) + ๐‘‘))
128127adantr 482 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โˆ’ 1) = ((๐ทโ€˜๐บ) + ๐‘‘))
129114, 128breqtrd 5135 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐ทโ€˜๐‘”) โ‰ค ((๐ทโ€˜๐บ) + ๐‘‘))
13071ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘ƒ โˆˆ Ring)
13117ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐บ โˆˆ ๐ต)
1325ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘… โˆˆ Ring)
133 ply1divex.i . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ ๐ผ โˆˆ ๐พ)
134133ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐ผ โˆˆ ๐พ)
135 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . 23 (coe1โ€˜๐‘”) = (coe1โ€˜๐‘”)
136 ply1divex.k . . . . . . . . . . . . . . . . . . . . . . 23 ๐พ = (Baseโ€˜๐‘…)
137135, 13, 11, 136coe1f 21605 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘” โˆˆ ๐ต โ†’ (coe1โ€˜๐‘”):โ„•0โŸถ๐พ)
138137adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (coe1โ€˜๐‘”):โ„•0โŸถ๐พ)
139 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘‘ โˆˆ โ„•0)
140106, 139nn0addcld 12485 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) โˆˆ โ„•0)
141138, 140ffvelcdmd 7040 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) โˆˆ ๐พ)
142 ply1divex.u . . . . . . . . . . . . . . . . . . . . 21 ยท = (.rโ€˜๐‘…)
143136, 142ringcl 19989 . . . . . . . . . . . . . . . . . . . 20 ((๐‘… โˆˆ Ring โˆง ๐ผ โˆˆ ๐พ โˆง ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) โˆˆ ๐พ) โ†’ (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) โˆˆ ๐พ)
144132, 134, 141, 143syl3anc 1372 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) โˆˆ ๐พ)
145 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (var1โ€˜๐‘…) = (var1โ€˜๐‘…)
146 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 ( ยท๐‘  โ€˜๐‘ƒ) = ( ยท๐‘  โ€˜๐‘ƒ)
147 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (mulGrpโ€˜๐‘ƒ) = (mulGrpโ€˜๐‘ƒ)
148 eqid 2733 . . . . . . . . . . . . . . . . . . . 20 (.gโ€˜(mulGrpโ€˜๐‘ƒ)) = (.gโ€˜(mulGrpโ€˜๐‘ƒ))
149136, 11, 145, 146, 147, 148, 13ply1tmcl 21666 . . . . . . . . . . . . . . . . . . 19 ((๐‘… โˆˆ Ring โˆง (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) โˆˆ ๐พ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต)
150132, 144, 139, 149syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต)
15113, 75ringcl 19989 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ Ring โˆง ๐บ โˆˆ ๐ต โˆง ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต) โ†’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
152130, 131, 150, 151syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
153152adantrr 716 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
154106nn0red 12482 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„)
155154leidd 11729 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜๐บ) โ‰ค (๐ทโ€˜๐บ))
15610, 136, 11, 145, 146, 147, 148deg1tmle 25505 . . . . . . . . . . . . . . . . . . 19 ((๐‘… โˆˆ Ring โˆง (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) โˆˆ ๐พ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ (๐ทโ€˜((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ‰ค ๐‘‘)
157132, 144, 139, 156syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ‰ค ๐‘‘)
15811, 10, 132, 13, 75, 131, 150, 106, 139, 155, 157deg1mulle2 25497 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ‰ค ((๐ทโ€˜๐บ) + ๐‘‘))
159158adantrr 716 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐ทโ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ‰ค ((๐ทโ€˜๐บ) + ๐‘‘))
160 eqid 2733 . . . . . . . . . . . . . . . 16 (coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) = (coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))
161 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (0gโ€˜๐‘…) = (0gโ€˜๐‘…)
162161, 136, 11, 145, 146, 147, 148, 13, 75, 142, 131, 132, 144, 139, 106coe1tmmul2fv 21672 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))โ€˜(๐‘‘ + (๐ทโ€˜๐บ))) = (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))))
163106nn0cnd 12483 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐ทโ€˜๐บ) โˆˆ โ„‚)
164117ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘‘ โˆˆ โ„‚)
165163, 164addcomd 11365 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐บ) + ๐‘‘) = (๐‘‘ + (๐ทโ€˜๐บ)))
166165fveq2d 6850 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) = ((coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))โ€˜(๐‘‘ + (๐ทโ€˜๐บ))))
167 ply1divex.g3 . . . . . . . . . . . . . . . . . . . . 21 (๐œ‘ โ†’ (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) = 1 )
168167oveq1d 7376 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = ( 1 ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))))
169168ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = ( 1 ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))))
170 eqid 2733 . . . . . . . . . . . . . . . . . . . . . . . 24 (coe1โ€˜๐บ) = (coe1โ€˜๐บ)
171170, 13, 11, 136coe1f 21605 . . . . . . . . . . . . . . . . . . . . . . 23 (๐บ โˆˆ ๐ต โ†’ (coe1โ€˜๐บ):โ„•0โŸถ๐พ)
17217, 171syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (coe1โ€˜๐บ):โ„•0โŸถ๐พ)
173172ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (coe1โ€˜๐บ):โ„•0โŸถ๐พ)
174173, 106ffvelcdmd 7040 . . . . . . . . . . . . . . . . . . . 20 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) โˆˆ ๐พ)
175136, 142ringass 19992 . . . . . . . . . . . . . . . . . . . 20 ((๐‘… โˆˆ Ring โˆง (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) โˆˆ ๐พ โˆง ๐ผ โˆˆ ๐พ โˆง ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) โˆˆ ๐พ)) โ†’ ((((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))))
176132, 174, 134, 141, 175syl13anc 1373 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท ๐ผ) ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))))
177 ply1divex.o . . . . . . . . . . . . . . . . . . . . 21 1 = (1rโ€˜๐‘…)
178136, 142, 177ringlidm 20000 . . . . . . . . . . . . . . . . . . . 20 ((๐‘… โˆˆ Ring โˆง ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) โˆˆ ๐พ) โ†’ ( 1 ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))
179132, 141, 178syl2anc 585 . . . . . . . . . . . . . . . . . . 19 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ( 1 ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘))) = ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))
180169, 176, 1793eqtr3rd 2782 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) = (((coe1โ€˜๐บ)โ€˜(๐ทโ€˜๐บ)) ยท (๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))))
181162, 166, 1803eqtr4rd 2784 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) = ((coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))
182181adantrr 716 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)) = ((coe1โ€˜(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))
18310, 11, 13, 82, 102, 103, 104, 129, 153, 159, 135, 160, 182deg1sublt 25498 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) < ((๐ทโ€˜๐บ) + ๐‘‘))
184183adantlrr 720 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) < ((๐ทโ€˜๐บ) + ๐‘‘))
185 fveq2 6846 . . . . . . . . . . . . . . . . 17 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ (๐ทโ€˜๐‘“) = (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
186185breq1d 5119 . . . . . . . . . . . . . . . 16 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†” (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) < ((๐ทโ€˜๐บ) + ๐‘‘)))
187 fvoveq1 7384 . . . . . . . . . . . . . . . . . 18 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) = (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))))
188187breq1d 5119 . . . . . . . . . . . . . . . . 17 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ ((๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
189188rexbidv 3172 . . . . . . . . . . . . . . . 16 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ (โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
190186, 189imbi12d 345 . . . . . . . . . . . . . . 15 (๐‘“ = (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โ†’ (((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
191 simplrr 777 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
19281ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘ƒ โˆˆ Grp)
193 simpr 486 . . . . . . . . . . . . . . . . . 18 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ ๐‘” โˆˆ ๐ต)
19413, 82grpsubcl 18835 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ Grp โˆง ๐‘” โˆˆ ๐ต โˆง (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต) โ†’ (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆˆ ๐ต)
195192, 193, 152, 194syl3anc 1372 . . . . . . . . . . . . . . . . 17 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆˆ ๐ต)
196195adantrr 716 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆˆ ๐ต)
197196adantlrr 720 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆˆ ๐ต)
198190, 191, 197rspcdva 3584 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ ((๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
199184, 198mpd 15 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
20071ad3antrrr 729 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ๐‘ƒ โˆˆ Ring)
201 simpr 486 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ๐‘ž โˆˆ ๐ต)
202150adantr 482 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต)
203 eqid 2733 . . . . . . . . . . . . . . . . . . 19 (+gโ€˜๐‘ƒ) = (+gโ€˜๐‘ƒ)
20413, 203ringacl 20007 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ Ring โˆง ๐‘ž โˆˆ ๐ต โˆง ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต) โ†’ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
205200, 201, 202, 204syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
20681ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ๐‘ƒ โˆˆ Grp)
207 simplr 768 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ๐‘” โˆˆ ๐ต)
208152adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต)
20917ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ๐บ โˆˆ ๐ต)
21013, 75ringcl 19989 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ Ring โˆง ๐บ โˆˆ ๐ต โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐บ โˆ™ ๐‘ž) โˆˆ ๐ต)
211200, 209, 201, 210syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐บ โˆ™ ๐‘ž) โˆˆ ๐ต)
21213, 203, 82grpsubsub4 18848 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ƒ โˆˆ Grp โˆง (๐‘” โˆˆ ๐ต โˆง (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต โˆง (๐บ โˆ™ ๐‘ž) โˆˆ ๐ต)) โ†’ ((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž)) = (๐‘” โˆ’ ((๐บ โˆ™ ๐‘ž)(+gโ€˜๐‘ƒ)(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
213206, 207, 208, 211, 212syl13anc 1373 . . . . . . . . . . . . . . . . . . . . 21 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž)) = (๐‘” โˆ’ ((๐บ โˆ™ ๐‘ž)(+gโ€˜๐‘ƒ)(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
21413, 203, 75ringdi 19995 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ Ring โˆง (๐บ โˆˆ ๐ต โˆง ๐‘ž โˆˆ ๐ต โˆง ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))) โˆˆ ๐ต)) โ†’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) = ((๐บ โˆ™ ๐‘ž)(+gโ€˜๐‘ƒ)(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))
215200, 209, 201, 202, 214syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) = ((๐บ โˆ™ ๐‘ž)(+gโ€˜๐‘ƒ)(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))
216215oveq2d 7377 . . . . . . . . . . . . . . . . . . . . 21 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))) = (๐‘” โˆ’ ((๐บ โˆ™ ๐‘ž)(+gโ€˜๐‘ƒ)(๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
217213, 216eqtr4d 2776 . . . . . . . . . . . . . . . . . . . 20 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž)) = (๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
218217fveq2d 6850 . . . . . . . . . . . . . . . . . . 19 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) = (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))))
219218breq1d 5119 . . . . . . . . . . . . . . . . . 18 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))) < (๐ทโ€˜๐บ)))
220219biimpd 228 . . . . . . . . . . . . . . . . 17 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†’ (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))) < (๐ทโ€˜๐บ)))
221 oveq2 7369 . . . . . . . . . . . . . . . . . . . . 21 (๐‘Ÿ = (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ†’ (๐บ โˆ™ ๐‘Ÿ) = (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))
222221oveq2d 7377 . . . . . . . . . . . . . . . . . . . 20 (๐‘Ÿ = (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ†’ (๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ)) = (๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))))))
223222fveq2d 6850 . . . . . . . . . . . . . . . . . . 19 (๐‘Ÿ = (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ†’ (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) = (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))))
224223breq1d 5119 . . . . . . . . . . . . . . . . . 18 (๐‘Ÿ = (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โ†’ ((๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))) < (๐ทโ€˜๐บ)))
225224rspcev 3583 . . . . . . . . . . . . . . . . 17 (((๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…)))) โˆˆ ๐ต โˆง (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ (๐‘ž(+gโ€˜๐‘ƒ)((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))))) < (๐ทโ€˜๐บ)) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ))
226205, 220, 225syl6an 683 . . . . . . . . . . . . . . . 16 ((((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โˆง ๐‘ž โˆˆ ๐ต) โ†’ ((๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
227226rexlimdva 3149 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง ๐‘” โˆˆ ๐ต) โ†’ (โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
228227adantrr 716 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
229228adantlrr 720 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ (โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜((๐‘” โˆ’ (๐บ โˆ™ ((๐ผ ยท ((coe1โ€˜๐‘”)โ€˜((๐ทโ€˜๐บ) + ๐‘‘)))( ยท๐‘  โ€˜๐‘ƒ)(๐‘‘(.gโ€˜(mulGrpโ€˜๐‘ƒ))(var1โ€˜๐‘…))))) โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
230199, 229mpd 15 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง (๐‘” โˆˆ ๐ต โˆง (๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)))) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ))
231230expr 458 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โˆง ๐‘” โˆˆ ๐ต) โ†’ ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
232231ralrimiva 3140 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โ†’ โˆ€๐‘” โˆˆ ๐ต ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
233 fveq2 6846 . . . . . . . . . . . . 13 (๐‘” = ๐‘“ โ†’ (๐ทโ€˜๐‘”) = (๐ทโ€˜๐‘“))
234233breq1d 5119 . . . . . . . . . . . 12 (๐‘” = ๐‘“ โ†’ ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†” (๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1))))
235 fvoveq1 7384 . . . . . . . . . . . . . . 15 (๐‘” = ๐‘“ โ†’ (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) = (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))))
236235breq1d 5119 . . . . . . . . . . . . . 14 (๐‘” = ๐‘“ โ†’ ((๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
237236rexbidv 3172 . . . . . . . . . . . . 13 (๐‘” = ๐‘“ โ†’ (โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)))
238 oveq2 7369 . . . . . . . . . . . . . . . . 17 (๐‘Ÿ = ๐‘ž โ†’ (๐บ โˆ™ ๐‘Ÿ) = (๐บ โˆ™ ๐‘ž))
239238oveq2d 7377 . . . . . . . . . . . . . . . 16 (๐‘Ÿ = ๐‘ž โ†’ (๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ)) = (๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž)))
240239fveq2d 6850 . . . . . . . . . . . . . . 15 (๐‘Ÿ = ๐‘ž โ†’ (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))) = (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))))
241240breq1d 5119 . . . . . . . . . . . . . 14 (๐‘Ÿ = ๐‘ž โ†’ ((๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
242241cbvrexvw 3225 . . . . . . . . . . . . 13 (โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
243237, 242bitrdi 287 . . . . . . . . . . . 12 (๐‘” = ๐‘“ โ†’ (โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ) โ†” โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
244234, 243imbi12d 345 . . . . . . . . . . 11 (๐‘” = ๐‘“ โ†’ (((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)) โ†” ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
245244cbvralvw 3224 . . . . . . . . . 10 (โˆ€๐‘” โˆˆ ๐ต ((๐ทโ€˜๐‘”) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘Ÿ โˆˆ ๐ต (๐ทโ€˜(๐‘” โˆ’ (๐บ โˆ™ ๐‘Ÿ))) < (๐ทโ€˜๐บ)) โ†” โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
246232, 245sylib 217 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘‘ โˆˆ โ„•0 โˆง โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))) โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
247246exp32 422 . . . . . . . 8 (๐œ‘ โ†’ (๐‘‘ โˆˆ โ„•0 โ†’ (โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
248247com12 32 . . . . . . 7 (๐‘‘ โˆˆ โ„•0 โ†’ (๐œ‘ โ†’ (โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)) โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
249248a2d 29 . . . . . 6 (๐‘‘ โˆˆ โ„•0 โ†’ ((๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))) โ†’ (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + (๐‘‘ + 1)) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))))
25059, 64, 69, 64, 99, 249nn0ind 12606 . . . . 5 (๐‘‘ โˆˆ โ„•0 โ†’ (๐œ‘ โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))))
251250impcom 409 . . . 4 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ โˆ€๐‘“ โˆˆ ๐ต ((๐ทโ€˜๐‘“) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐‘“ โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
2527adantr 482 . . . 4 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ๐น โˆˆ ๐ต)
25354, 251, 252rspcdva 3584 . . 3 ((๐œ‘ โˆง ๐‘‘ โˆˆ โ„•0) โ†’ ((๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
254253rexlimdva 3149 . 2 (๐œ‘ โ†’ (โˆƒ๐‘‘ โˆˆ โ„•0 (๐ทโ€˜๐น) < ((๐ทโ€˜๐บ) + ๐‘‘) โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ)))
25548, 254mpd 15 1 (๐œ‘ โ†’ โˆƒ๐‘ž โˆˆ ๐ต (๐ทโ€˜(๐น โˆ’ (๐บ โˆ™ ๐‘ž))) < (๐ทโ€˜๐บ))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070   โˆช cun 3912   โŠ† wss 3914  {csn 4590   class class class wbr 5109  โŸถwf 6496  โ€˜cfv 6500  (class class class)co 7361  โ„‚cc 11057  โ„cr 11058  0cc0 11059  1c1 11060   + caddc 11062  -โˆžcmnf 11195   < clt 11197   โ‰ค cle 11198   โˆ’ cmin 11393  โ„•cn 12161  โ„•0cn0 12421  โ„คcz 12507  Basecbs 17091  +gcplusg 17141  .rcmulr 17142   ยท๐‘  cvsca 17145  0gc0g 17329  Grpcgrp 18756  -gcsg 18758  .gcmg 18880  mulGrpcmgp 19904  1rcur 19921  Ringcrg 19972  var1cv1 21570  Poly1cpl1 21571  coe1cco1 21572   deg1 cdg1 25439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-addf 11138  ax-mulf 11139
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-iin 4961  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-ofr 7622  df-om 7807  df-1st 7925  df-2nd 7926  df-supp 8097  df-tpos 8161  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-er 8654  df-map 8773  df-pm 8774  df-ixp 8842  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fsupp 9312  df-sup 9386  df-oi 9454  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-nn 12162  df-2 12224  df-3 12225  df-4 12226  df-5 12227  df-6 12228  df-7 12229  df-8 12230  df-9 12231  df-n0 12422  df-z 12508  df-dec 12627  df-uz 12772  df-fz 13434  df-fzo 13577  df-seq 13916  df-hash 14240  df-struct 17027  df-sets 17044  df-slot 17062  df-ndx 17074  df-base 17092  df-ress 17121  df-plusg 17154  df-mulr 17155  df-starv 17156  df-sca 17157  df-vsca 17158  df-ip 17159  df-tset 17160  df-ple 17161  df-ds 17163  df-unif 17164  df-hom 17165  df-cco 17166  df-0g 17331  df-gsum 17332  df-prds 17337  df-pws 17339  df-mre 17474  df-mrc 17475  df-acs 17477  df-mgm 18505  df-sgrp 18554  df-mnd 18565  df-mhm 18609  df-submnd 18610  df-grp 18759  df-minusg 18760  df-sbg 18761  df-mulg 18881  df-subg 18933  df-ghm 19014  df-cntz 19105  df-cmn 19572  df-abl 19573  df-mgp 19905  df-ur 19922  df-ring 19974  df-cring 19975  df-oppr 20057  df-dvdsr 20078  df-unit 20079  df-invr 20109  df-subrg 20262  df-lmod 20367  df-lss 20437  df-rlreg 20776  df-cnfld 20820  df-psr 21334  df-mvr 21335  df-mpl 21336  df-opsr 21338  df-psr1 21574  df-vr1 21575  df-ply1 21576  df-coe1 21577  df-mdeg 25440  df-deg1 25441
This theorem is referenced by:  ply1divalg  25525
  Copyright terms: Public domain W3C validator