Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝐹 = 0 → (𝐷‘𝐹) = (𝐷‘ 0 )) |
2 | 1 | breq1d 4593 |
. . . 4
⊢ (𝐹 = 0 → ((𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) ↔ (𝐷‘ 0 ) < ((𝐷‘𝐺) + 𝑑))) |
3 | 2 | rexbidv 3034 |
. . 3
⊢ (𝐹 = 0 → (∃𝑑 ∈ ℕ0
(𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) ↔ ∃𝑑 ∈ ℕ0 (𝐷‘ 0 ) < ((𝐷‘𝐺) + 𝑑))) |
4 | | nnssnn0 11172 |
. . . . 5
⊢ ℕ
⊆ ℕ0 |
5 | | ply1divalg.r1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → 𝑅 ∈ Ring) |
7 | | ply1divalg.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐵) |
9 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → 𝐹 ≠ 0 ) |
10 | | ply1divalg.d |
. . . . . . . . . 10
⊢ 𝐷 = ( deg1
‘𝑅) |
11 | | ply1divalg.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
12 | | ply1divalg.z |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑃) |
13 | | ply1divalg.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑃) |
14 | 10, 11, 12, 13 | deg1nn0cl 23652 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈
ℕ0) |
15 | 6, 8, 9, 14 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈
ℕ0) |
16 | 15 | nn0red 11229 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℝ) |
17 | | ply1divalg.g1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
18 | | ply1divalg.g2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ≠ 0 ) |
19 | 10, 11, 12, 13 | deg1nn0cl 23652 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → (𝐷‘𝐺) ∈
ℕ0) |
20 | 5, 17, 18, 19 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℕ0) |
21 | 20 | nn0red 11229 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐺) ∈ ℝ) |
22 | 21 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐺) ∈ ℝ) |
23 | 16, 22 | resubcld 10337 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → ((𝐷‘𝐹) − (𝐷‘𝐺)) ∈ ℝ) |
24 | | arch 11166 |
. . . . . 6
⊢ (((𝐷‘𝐹) − (𝐷‘𝐺)) ∈ ℝ → ∃𝑑 ∈ ℕ ((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑) |
25 | 23, 24 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → ∃𝑑 ∈ ℕ ((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑) |
26 | | ssrexv 3630 |
. . . . 5
⊢ (ℕ
⊆ ℕ0 → (∃𝑑 ∈ ℕ ((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑 → ∃𝑑 ∈ ℕ0 ((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑)) |
27 | 4, 25, 26 | mpsyl 66 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → ∃𝑑 ∈ ℕ0
((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑) |
28 | 16 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0) → (𝐷‘𝐹) ∈ ℝ) |
29 | 21 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0) → (𝐷‘𝐺) ∈ ℝ) |
30 | | nn0re 11178 |
. . . . . . . 8
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℝ) |
31 | 30 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0) → 𝑑 ∈
ℝ) |
32 | 28, 29, 31 | ltsubadd2d 10504 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0) → (((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑 ↔ (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑))) |
33 | 32 | biimpd 218 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹 ≠ 0 ) ∧ 𝑑 ∈ ℕ0) → (((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑 → (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑))) |
34 | 33 | reximdva 3000 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → (∃𝑑 ∈ ℕ0
((𝐷‘𝐹) − (𝐷‘𝐺)) < 𝑑 → ∃𝑑 ∈ ℕ0 (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑))) |
35 | 27, 34 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ≠ 0 ) → ∃𝑑 ∈ ℕ0
(𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑)) |
36 | | 0nn0 11184 |
. . . 4
⊢ 0 ∈
ℕ0 |
37 | 10, 11, 12 | deg1z 23651 |
. . . . . 6
⊢ (𝑅 ∈ Ring → (𝐷‘ 0 ) =
-∞) |
38 | 5, 37 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐷‘ 0 ) =
-∞) |
39 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
40 | | readdcl 9898 |
. . . . . . 7
⊢ (((𝐷‘𝐺) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((𝐷‘𝐺) + 0) ∈
ℝ) |
41 | 21, 39, 40 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((𝐷‘𝐺) + 0) ∈ ℝ) |
42 | | mnflt 11833 |
. . . . . 6
⊢ (((𝐷‘𝐺) + 0) ∈ ℝ → -∞ <
((𝐷‘𝐺) + 0)) |
43 | 41, 42 | syl 17 |
. . . . 5
⊢ (𝜑 → -∞ < ((𝐷‘𝐺) + 0)) |
44 | 38, 43 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → (𝐷‘ 0 ) < ((𝐷‘𝐺) + 0)) |
45 | | oveq2 6557 |
. . . . . 6
⊢ (𝑑 = 0 → ((𝐷‘𝐺) + 𝑑) = ((𝐷‘𝐺) + 0)) |
46 | 45 | breq2d 4595 |
. . . . 5
⊢ (𝑑 = 0 → ((𝐷‘ 0 ) < ((𝐷‘𝐺) + 𝑑) ↔ (𝐷‘ 0 ) < ((𝐷‘𝐺) + 0))) |
47 | 46 | rspcev 3282 |
. . . 4
⊢ ((0
∈ ℕ0 ∧ (𝐷‘ 0 ) < ((𝐷‘𝐺) + 0)) → ∃𝑑 ∈ ℕ0 (𝐷‘ 0 ) < ((𝐷‘𝐺) + 𝑑)) |
48 | 36, 44, 47 | sylancr 694 |
. . 3
⊢ (𝜑 → ∃𝑑 ∈ ℕ0 (𝐷‘ 0 ) < ((𝐷‘𝐺) + 𝑑)) |
49 | 3, 35, 48 | pm2.61ne 2867 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ ℕ0 (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑)) |
50 | 7 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → 𝐹 ∈ 𝐵) |
51 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑎 = 0 → ((𝐷‘𝐺) + 𝑎) = ((𝐷‘𝐺) + 0)) |
52 | 51 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑎 = 0 → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) ↔ (𝐷‘𝑓) < ((𝐷‘𝐺) + 0))) |
53 | 52 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑎 = 0 → (((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
54 | 53 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑎 = 0 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
55 | 54 | imbi2d 329 |
. . . . . 6
⊢ (𝑎 = 0 → ((𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) ↔ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
56 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑑 → ((𝐷‘𝐺) + 𝑎) = ((𝐷‘𝐺) + 𝑑)) |
57 | 56 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑎 = 𝑑 → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) ↔ (𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑))) |
58 | 57 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑎 = 𝑑 → (((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
59 | 58 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑎 = 𝑑 → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
60 | 59 | imbi2d 329 |
. . . . . 6
⊢ (𝑎 = 𝑑 → ((𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) ↔ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
61 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑑 + 1) → ((𝐷‘𝐺) + 𝑎) = ((𝐷‘𝐺) + (𝑑 + 1))) |
62 | 61 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑎 = (𝑑 + 1) → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) ↔ (𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)))) |
63 | 62 | imbi1d 330 |
. . . . . . . 8
⊢ (𝑎 = (𝑑 + 1) → (((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
64 | 63 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑎 = (𝑑 + 1) → (∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
65 | 64 | imbi2d 329 |
. . . . . 6
⊢ (𝑎 = (𝑑 + 1) → ((𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑎) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) ↔ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
66 | 11 | ply1ring 19439 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
67 | 5, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ Ring) |
68 | 13, 12 | ring0cl 18392 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ Ring → 0 ∈ 𝐵) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ 𝐵) |
70 | 69 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐵) ∧ (𝐷‘𝑓) < ((𝐷‘𝐺) + 0)) → 0 ∈ 𝐵) |
71 | | ply1divalg.t |
. . . . . . . . . . . . . . . . 17
⊢ ∙ =
(.r‘𝑃) |
72 | 13, 71, 12 | ringrz 18411 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵) → (𝐺 ∙ 0 ) = 0 ) |
73 | 67, 17, 72 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 ∙ 0 ) = 0 ) |
74 | 73 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑓 − (𝐺 ∙ 0 )) = (𝑓 − 0 )) |
75 | 74 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → (𝑓 − (𝐺 ∙ 0 )) = (𝑓 − 0 )) |
76 | | ringgrp 18375 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
77 | 67, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑃 ∈ Grp) |
78 | | ply1divalg.m |
. . . . . . . . . . . . . . 15
⊢ − =
(-g‘𝑃) |
79 | 13, 12, 78 | grpsubid1 17323 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ Grp ∧ 𝑓 ∈ 𝐵) → (𝑓 − 0 ) = 𝑓) |
80 | 77, 79 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → (𝑓 − 0 ) = 𝑓) |
81 | 75, 80 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → 𝑓 = (𝑓 − (𝐺 ∙ 0 ))) |
82 | 81 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → (𝐷‘𝑓) = (𝐷‘(𝑓 − (𝐺 ∙ 0 )))) |
83 | 20 | nn0cnd 11230 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘𝐺) ∈ ℂ) |
84 | 83 | addid1d 10115 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐷‘𝐺) + 0) = (𝐷‘𝐺)) |
85 | 84 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝐺) + 0) = (𝐷‘𝐺)) |
86 | 82, 85 | breq12d 4596 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) ↔ (𝐷‘(𝑓 − (𝐺 ∙ 0 ))) < (𝐷‘𝐺))) |
87 | 86 | biimpa 500 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐵) ∧ (𝐷‘𝑓) < ((𝐷‘𝐺) + 0)) → (𝐷‘(𝑓 − (𝐺 ∙ 0 ))) < (𝐷‘𝐺)) |
88 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 0 → (𝐺 ∙ 𝑞) = (𝐺 ∙ 0 )) |
89 | 88 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑞 = 0 → (𝑓 − (𝐺 ∙ 𝑞)) = (𝑓 − (𝐺 ∙ 0 ))) |
90 | 89 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑞 = 0 → (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) = (𝐷‘(𝑓 − (𝐺 ∙ 0 )))) |
91 | 90 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑞 = 0 → ((𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ (𝐷‘(𝑓 − (𝐺 ∙ 0 ))) < (𝐷‘𝐺))) |
92 | 91 | rspcev 3282 |
. . . . . . . . 9
⊢ (( 0 ∈ 𝐵 ∧ (𝐷‘(𝑓 − (𝐺 ∙ 0 ))) < (𝐷‘𝐺)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |
93 | 70, 87, 92 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐵) ∧ (𝐷‘𝑓) < ((𝐷‘𝐺) + 0)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |
94 | 93 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐵) → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
95 | 94 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 0) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
96 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐷‘𝐺) ∈ ℕ0 ∧ 𝑑 ∈ ℕ0)
→ ((𝐷‘𝐺) + 𝑑) ∈
ℕ0) |
97 | 20, 96 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝐷‘𝐺) + 𝑑) ∈
ℕ0) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ((𝐷‘𝐺) + 𝑑) ∈
ℕ0) |
99 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → 𝑅 ∈ Ring) |
100 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → 𝑔 ∈ 𝐵) |
101 | 10, 11, 13 | deg1cl 23647 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ 𝐵 → (𝐷‘𝑔) ∈ (ℕ0 ∪
{-∞})) |
102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘𝑔) ∈ (ℕ0 ∪
{-∞})) |
103 | 20 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘𝐺) ∈
ℕ0) |
104 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ0) |
105 | 104 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝑑 + 1) ∈
ℕ0) |
106 | 103, 105 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝐺) + (𝑑 + 1)) ∈
ℕ0) |
107 | 106 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝐺) + (𝑑 + 1)) ∈ ℤ) |
108 | | degltlem1 23636 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷‘𝑔) ∈ (ℕ0 ∪
{-∞}) ∧ ((𝐷‘𝐺) + (𝑑 + 1)) ∈ ℤ) → ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) ↔ (𝐷‘𝑔) ≤ (((𝐷‘𝐺) + (𝑑 + 1)) − 1))) |
109 | 102, 107,
108 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) ↔ (𝐷‘𝑔) ≤ (((𝐷‘𝐺) + (𝑑 + 1)) − 1))) |
110 | 109 | biimpd 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) → (𝐷‘𝑔) ≤ (((𝐷‘𝐺) + (𝑑 + 1)) − 1))) |
111 | 110 | impr 647 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐷‘𝑔) ≤ (((𝐷‘𝐺) + (𝑑 + 1)) − 1)) |
112 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝐷‘𝐺) ∈
ℕ0) |
113 | 112 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝐷‘𝐺) ∈ ℂ) |
114 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ∈ ℕ0
→ 𝑑 ∈
ℂ) |
115 | 114 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → 𝑑 ∈
ℂ) |
116 | | peano2cn 10087 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∈ ℂ → (𝑑 + 1) ∈
ℂ) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑑 + 1) ∈
ℂ) |
118 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → 1 ∈
ℂ) |
119 | 113, 117,
118 | addsubassd 10291 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (((𝐷‘𝐺) + (𝑑 + 1)) − 1) = ((𝐷‘𝐺) + ((𝑑 + 1) − 1))) |
120 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℂ |
121 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑑 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑑 + 1)
− 1) = 𝑑) |
122 | 115, 120,
121 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝑑 + 1) − 1) = 𝑑) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝐷‘𝐺) + ((𝑑 + 1) − 1)) = ((𝐷‘𝐺) + 𝑑)) |
124 | 119, 123 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (((𝐷‘𝐺) + (𝑑 + 1)) − 1) = ((𝐷‘𝐺) + 𝑑)) |
125 | 124 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (((𝐷‘𝐺) + (𝑑 + 1)) − 1) = ((𝐷‘𝐺) + 𝑑)) |
126 | 111, 125 | breqtrd 4609 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐷‘𝑔) ≤ ((𝐷‘𝐺) + 𝑑)) |
127 | 67 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑃 ∈ Ring) |
128 | 17 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
129 | 5 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑅 ∈ Ring) |
130 | | ply1divex.i |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐼 ∈ 𝐾) |
131 | 130 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝐼 ∈ 𝐾) |
132 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(coe1‘𝑔) = (coe1‘𝑔) |
133 | | ply1divex.k |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐾 = (Base‘𝑅) |
134 | 132, 13, 11, 133 | coe1f 19402 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔 ∈ 𝐵 → (coe1‘𝑔):ℕ0⟶𝐾) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (coe1‘𝑔):ℕ0⟶𝐾) |
136 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑑 ∈ ℕ0) |
137 | 103, 136 | nn0addcld 11232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝐺) + 𝑑) ∈
ℕ0) |
138 | 135, 137 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) ∈ 𝐾) |
139 | | ply1divex.u |
. . . . . . . . . . . . . . . . . . . . 21
⊢ · =
(.r‘𝑅) |
140 | 133, 139 | ringcl 18384 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝐾 ∧ ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) ∈ 𝐾) → (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) ∈ 𝐾) |
141 | 129, 131,
138, 140 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) ∈ 𝐾) |
142 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(var1‘𝑅) = (var1‘𝑅) |
143 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (
·𝑠 ‘𝑃) = ( ·𝑠
‘𝑃) |
144 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(mulGrp‘𝑃) =
(mulGrp‘𝑃) |
145 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(.g‘(mulGrp‘𝑃)) =
(.g‘(mulGrp‘𝑃)) |
146 | 133, 11, 142, 143, 144, 145, 13 | ply1tmcl 19463 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Ring ∧ (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) ∈ 𝐾 ∧ 𝑑 ∈ ℕ0) → ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵) |
147 | 129, 141,
136, 146 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵) |
148 | 13, 71 | ringcl 18384 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵) → (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
149 | 127, 128,
147, 148 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
150 | 149 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
151 | 103 | nn0red 11229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘𝐺) ∈ ℝ) |
152 | 151 | leidd 10473 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘𝐺) ≤ (𝐷‘𝐺)) |
153 | 10, 133, 11, 142, 143, 144, 145 | deg1tmle 23681 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Ring ∧ (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) ∈ 𝐾 ∧ 𝑑 ∈ ℕ0) → (𝐷‘((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ≤ 𝑑) |
154 | 129, 141,
136, 153 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ≤ 𝑑) |
155 | 11, 10, 129, 13, 71, 128, 147, 103, 136, 152, 154 | deg1mulle2 23673 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ≤ ((𝐷‘𝐺) + 𝑑)) |
156 | 155 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐷‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ≤ ((𝐷‘𝐺) + 𝑑)) |
157 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) =
(coe1‘(𝐺
∙
((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) |
158 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0g‘𝑅) = (0g‘𝑅) |
159 | 158, 133,
11, 142, 143, 144, 145, 13, 71, 139, 128, 129, 141, 136, 103 | coe1tmmul2fv 19469 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))‘(𝑑 + (𝐷‘𝐺))) = (((coe1‘𝐺)‘(𝐷‘𝐺)) · (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))))) |
160 | 103 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝐷‘𝐺) ∈ ℂ) |
161 | 114 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑑 ∈ ℂ) |
162 | 160, 161 | addcomd 10117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝐺) + 𝑑) = (𝑑 + (𝐷‘𝐺))) |
163 | 162 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))‘((𝐷‘𝐺) + 𝑑)) = ((coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))‘(𝑑 + (𝐷‘𝐺)))) |
164 | | ply1divex.g3 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) = 1 ) |
165 | 164 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
((((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = ( 1 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))) |
166 | 165 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = ( 1 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))) |
167 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
168 | 167, 13, 11, 133 | coe1f 19402 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶𝐾) |
169 | 17, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 →
(coe1‘𝐺):ℕ0⟶𝐾) |
170 | 169 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶𝐾) |
171 | 170, 103 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝐾) |
172 | 133, 139 | ringass 18387 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧
(((coe1‘𝐺)‘(𝐷‘𝐺)) ∈ 𝐾 ∧ 𝐼 ∈ 𝐾 ∧ ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) ∈ 𝐾)) → ((((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = (((coe1‘𝐺)‘(𝐷‘𝐺)) · (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))))) |
173 | 129, 171,
131, 138, 172 | syl13anc 1320 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((((coe1‘𝐺)‘(𝐷‘𝐺)) · 𝐼) ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = (((coe1‘𝐺)‘(𝐷‘𝐺)) · (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))))) |
174 | | ply1divex.o |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 =
(1r‘𝑅) |
175 | 133, 139,
174 | ringlidm 18394 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Ring ∧
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) ∈ 𝐾) → ( 1 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) |
176 | 129, 138,
175 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ( 1 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) = ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))) |
177 | 166, 173,
176 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) = (((coe1‘𝐺)‘(𝐷‘𝐺)) · (𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑))))) |
178 | 159, 163,
177 | 3eqtr4rd 2655 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) = ((coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))‘((𝐷‘𝐺) + 𝑑))) |
179 | 178 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)) = ((coe1‘(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))‘((𝐷‘𝐺) + 𝑑))) |
180 | 10, 11, 13, 78, 98, 99, 100, 126, 150, 156, 132, 157, 179 | deg1sublt 23674 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑)) |
181 | 180 | adantlrr 753 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑)) |
182 | 77 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑃 ∈ Grp) |
183 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → 𝑔 ∈ 𝐵) |
184 | 13, 78 | grpsubcl 17318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Grp ∧ 𝑔 ∈ 𝐵 ∧ (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) → (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ∈ 𝐵) |
185 | 182, 183,
149, 184 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ∈ 𝐵) |
186 | 185 | adantrr 749 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ∈ 𝐵) |
187 | 186 | adantlrr 753 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ∈ 𝐵) |
188 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
189 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → (𝐷‘𝑓) = (𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
190 | 189 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) ↔ (𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑))) |
191 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → (𝑓 − (𝐺 ∙ 𝑞)) = ((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) |
192 | 191 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) = (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞)))) |
193 | 192 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → ((𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
194 | 193 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → (∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ ∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
195 | 190, 194 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) → (((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ((𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
196 | 195 | rspcva 3280 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) ∈ 𝐵 ∧ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) → ((𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
197 | 187, 188,
196 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ((𝐷‘(𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
198 | 181, 197 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |
199 | 67 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Ring) |
200 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → 𝑞 ∈ 𝐵) |
201 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵) |
202 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(+g‘𝑃) = (+g‘𝑃) |
203 | 13, 202 | ringacl 18401 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Ring ∧ 𝑞 ∈ 𝐵 ∧ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵) → (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
204 | 199, 200,
201, 203 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
205 | 77 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → 𝑃 ∈ Grp) |
206 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → 𝑔 ∈ 𝐵) |
207 | 149 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵) |
208 | 17 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
209 | 13, 71 | ringcl 18384 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (𝐺 ∙ 𝑞) ∈ 𝐵) |
210 | 199, 208,
200, 209 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝐺 ∙ 𝑞) ∈ 𝐵) |
211 | 13, 202, 78 | grpsubsub4 17331 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃 ∈ Grp ∧ (𝑔 ∈ 𝐵 ∧ (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵 ∧ (𝐺 ∙ 𝑞) ∈ 𝐵)) → ((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞)) = (𝑔 − ((𝐺 ∙ 𝑞)(+g‘𝑃)(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
212 | 205, 206,
207, 210, 211 | syl13anc 1320 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞)) = (𝑔 − ((𝐺 ∙ 𝑞)(+g‘𝑃)(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
213 | 13, 202, 71 | ringdi 18389 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ Ring ∧ (𝐺 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ∈ 𝐵)) → (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) = ((𝐺 ∙ 𝑞)(+g‘𝑃)(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
214 | 199, 208,
200, 201, 213 | syl13anc 1320 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) = ((𝐺 ∙ 𝑞)(+g‘𝑃)(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
215 | 214 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) = (𝑔 − ((𝐺 ∙ 𝑞)(+g‘𝑃)(𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
216 | 212, 215 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞)) = (𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
217 | 216 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) = (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))))) |
218 | 217 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) < (𝐷‘𝐺))) |
219 | 218 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) → (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) < (𝐷‘𝐺))) |
220 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) → (𝐺 ∙ 𝑟) = (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))) |
221 | 220 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) → (𝑔 − (𝐺 ∙ 𝑟)) = (𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) |
222 | 221 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 = (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) → (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) = (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))))))) |
223 | 222 | breq1d 4593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) → ((𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) < (𝐷‘𝐺))) |
224 | 223 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅)))) ∈ 𝐵 ∧ (𝐷‘(𝑔 − (𝐺 ∙ (𝑞(+g‘𝑃)((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))))) < (𝐷‘𝐺)) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺)) |
225 | 204, 219,
224 | syl6an 566 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) ∧ 𝑞 ∈ 𝐵) → ((𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
226 | 225 | rexlimdva 3013 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑔 ∈ 𝐵) → (∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
227 | 226 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
228 | 227 | adantlrr 753 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → (∃𝑞 ∈ 𝐵 (𝐷‘((𝑔 − (𝐺 ∙ ((𝐼 ·
((coe1‘𝑔)‘((𝐷‘𝐺) + 𝑑)))( ·𝑠
‘𝑃)(𝑑(.g‘(mulGrp‘𝑃))(var1‘𝑅))))) − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
229 | 198, 228 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ (𝑔 ∈ 𝐵 ∧ (𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)))) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺)) |
230 | 229 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) ∧ 𝑔 ∈ 𝐵) → ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
231 | 230 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) → ∀𝑔 ∈ 𝐵 ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
232 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → (𝐷‘𝑔) = (𝐷‘𝑓)) |
233 | 232 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) ↔ (𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)))) |
234 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑓 → (𝑔 − (𝐺 ∙ 𝑟)) = (𝑓 − (𝐺 ∙ 𝑟))) |
235 | 234 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑓 → (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) = (𝐷‘(𝑓 − (𝐺 ∙ 𝑟)))) |
236 | 235 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑓 → ((𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ (𝐷‘(𝑓 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
237 | 236 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑓 → (∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ ∃𝑟 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺))) |
238 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑞 → (𝐺 ∙ 𝑟) = (𝐺 ∙ 𝑞)) |
239 | 238 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑞 → (𝑓 − (𝐺 ∙ 𝑟)) = (𝑓 − (𝐺 ∙ 𝑞))) |
240 | 239 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑞 → (𝐷‘(𝑓 − (𝐺 ∙ 𝑟))) = (𝐷‘(𝑓 − (𝐺 ∙ 𝑞)))) |
241 | 240 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = 𝑞 → ((𝐷‘(𝑓 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
242 | 241 | cbvrexv 3148 |
. . . . . . . . . . . . 13
⊢
(∃𝑟 ∈
𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |
243 | 237, 242 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺) ↔ ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
244 | 233, 243 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → (((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺)) ↔ ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
245 | 244 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑔 ∈
𝐵 ((𝐷‘𝑔) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑟 ∈ 𝐵 (𝐷‘(𝑔 − (𝐺 ∙ 𝑟))) < (𝐷‘𝐺)) ↔ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
246 | 231, 245 | sylib 207 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ0 ∧
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
247 | 246 | exp32 629 |
. . . . . . . 8
⊢ (𝜑 → (𝑑 ∈ ℕ0 →
(∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
248 | 247 | com12 32 |
. . . . . . 7
⊢ (𝑑 ∈ ℕ0
→ (𝜑 →
(∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
249 | 248 | a2d 29 |
. . . . . 6
⊢ (𝑑 ∈ ℕ0
→ ((𝜑 →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) → (𝜑 → ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + (𝑑 + 1)) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))))) |
250 | 55, 60, 65, 60, 95, 249 | nn0ind 11348 |
. . . . 5
⊢ (𝑑 ∈ ℕ0
→ (𝜑 →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
251 | 250 | impcom 445 |
. . . 4
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
252 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (𝐷‘𝑓) = (𝐷‘𝐹)) |
253 | 252 | breq1d 4593 |
. . . . . 6
⊢ (𝑓 = 𝐹 → ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) ↔ (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑))) |
254 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓 − (𝐺 ∙ 𝑞)) = (𝐹 − (𝐺 ∙ 𝑞))) |
255 | 254 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) = (𝐷‘(𝐹 − (𝐺 ∙ 𝑞)))) |
256 | 255 | breq1d 4593 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ((𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
257 | 256 | rexbidv 3034 |
. . . . . 6
⊢ (𝑓 = 𝐹 → (∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺) ↔ ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
258 | 253, 257 | imbi12d 333 |
. . . . 5
⊢ (𝑓 = 𝐹 → (((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) ↔ ((𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)))) |
259 | 258 | rspcva 3280 |
. . . 4
⊢ ((𝐹 ∈ 𝐵 ∧ ∀𝑓 ∈ 𝐵 ((𝐷‘𝑓) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝑓 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) → ((𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
260 | 50, 251, 259 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
261 | 260 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑑 ∈ ℕ0 (𝐷‘𝐹) < ((𝐷‘𝐺) + 𝑑) → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺))) |
262 | 49, 261 | mpd 15 |
1
⊢ (𝜑 → ∃𝑞 ∈ 𝐵 (𝐷‘(𝐹 − (𝐺 ∙ 𝑞))) < (𝐷‘𝐺)) |