Step | Hyp | Ref
| Expression |
1 | | recexpr 7600 |
. . . . 5
⊢ (𝐶 ∈ P →
∃𝑦 ∈
P (𝐶
·P 𝑦) =
1P) |
2 | 1 | 3ad2ant3 1015 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ∃𝑦 ∈ P (𝐶 ·P 𝑦) =
1P) |
3 | 2 | adantr 274 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) → ∃𝑦 ∈ P (𝐶 ·P 𝑦) =
1P) |
4 | | ltexpri 7575 |
. . . . 5
⊢ ((𝐶
·P 𝐴)<P (𝐶
·P 𝐵) → ∃𝑥 ∈ P ((𝐶 ·P 𝐴) +P
𝑥) = (𝐶 ·P 𝐵)) |
5 | 4 | ad2antlr 486 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) →
∃𝑥 ∈
P ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵)) |
6 | | simplll 528 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝐴 ∈ P ∧ 𝐵 ∈ P ∧
𝐶 ∈
P)) |
7 | 6 | simp1d 1004 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝐴 ∈ P) |
8 | | simplrl 530 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝑦 ∈ P) |
9 | | simprl 526 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝑥 ∈ P) |
10 | | mulclpr 7534 |
. . . . . . 7
⊢ ((𝑦 ∈ P ∧
𝑥 ∈ P)
→ (𝑦
·P 𝑥) ∈ P) |
11 | 8, 9, 10 | syl2anc 409 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P 𝑥) ∈
P) |
12 | | ltaddpr 7559 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
(𝑦
·P 𝑥) ∈ P) → 𝐴<P
(𝐴
+P (𝑦 ·P 𝑥))) |
13 | 7, 11, 12 | syl2anc 409 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝐴<P (𝐴 +P
(𝑦
·P 𝑥))) |
14 | | simprr 527 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝐶 ·P 𝐴) +P
𝑥) = (𝐶 ·P 𝐵)) |
15 | 14 | oveq2d 5869 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P ((𝐶
·P 𝐴) +P 𝑥)) = (𝑦 ·P (𝐶
·P 𝐵))) |
16 | 6 | simp3d 1006 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝐶 ∈ P) |
17 | | mulclpr 7534 |
. . . . . . . . 9
⊢ ((𝐶 ∈ P ∧
𝐴 ∈ P)
→ (𝐶
·P 𝐴) ∈ P) |
18 | 16, 7, 17 | syl2anc 409 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝐶 ·P 𝐴) ∈
P) |
19 | | distrprg 7550 |
. . . . . . . 8
⊢ ((𝑦 ∈ P ∧
(𝐶
·P 𝐴) ∈ P ∧ 𝑥 ∈ P) →
(𝑦
·P ((𝐶 ·P 𝐴) +P
𝑥)) = ((𝑦 ·P (𝐶
·P 𝐴)) +P (𝑦
·P 𝑥))) |
20 | 8, 18, 9, 19 | syl3anc 1233 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P ((𝐶
·P 𝐴) +P 𝑥)) = ((𝑦 ·P (𝐶
·P 𝐴)) +P (𝑦
·P 𝑥))) |
21 | | mulassprg 7543 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
𝐶 ∈ P
∧ 𝐴 ∈
P) → ((𝑦
·P 𝐶) ·P 𝐴) = (𝑦 ·P (𝐶
·P 𝐴))) |
22 | 8, 16, 7, 21 | syl3anc 1233 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝑦 ·P 𝐶)
·P 𝐴) = (𝑦 ·P (𝐶
·P 𝐴))) |
23 | 22 | oveq1d 5868 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (((𝑦 ·P 𝐶)
·P 𝐴) +P (𝑦
·P 𝑥)) = ((𝑦 ·P (𝐶
·P 𝐴)) +P (𝑦
·P 𝑥))) |
24 | | mulcomprg 7542 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ P ∧
𝐶 ∈ P)
→ (𝑦
·P 𝐶) = (𝐶 ·P 𝑦)) |
25 | 8, 16, 24 | syl2anc 409 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P 𝐶) = (𝐶 ·P 𝑦)) |
26 | | simplrr 531 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝐶 ·P 𝑦) =
1P) |
27 | 25, 26 | eqtrd 2203 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P 𝐶) =
1P) |
28 | 27 | oveq1d 5868 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝑦 ·P 𝐶)
·P 𝐴) = (1P
·P 𝐴)) |
29 | | 1pr 7516 |
. . . . . . . . . . . 12
⊢
1P ∈ P |
30 | | mulcomprg 7542 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
1P ∈ P) → (𝐴 ·P
1P) = (1P
·P 𝐴)) |
31 | 29, 30 | mpan2 423 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ P →
(𝐴
·P 1P) =
(1P ·P 𝐴)) |
32 | | 1idpr 7554 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ P →
(𝐴
·P 1P) = 𝐴) |
33 | 31, 32 | eqtr3d 2205 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
(1P ·P 𝐴) = 𝐴) |
34 | 7, 33 | syl 14 |
. . . . . . . . 9
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) →
(1P ·P 𝐴) = 𝐴) |
35 | 28, 34 | eqtrd 2203 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝑦 ·P 𝐶)
·P 𝐴) = 𝐴) |
36 | 35 | oveq1d 5868 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (((𝑦 ·P 𝐶)
·P 𝐴) +P (𝑦
·P 𝑥)) = (𝐴 +P (𝑦
·P 𝑥))) |
37 | 20, 23, 36 | 3eqtr2d 2209 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P ((𝐶
·P 𝐴) +P 𝑥)) = (𝐴 +P (𝑦
·P 𝑥))) |
38 | 27 | oveq1d 5868 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝑦 ·P 𝐶)
·P 𝐵) = (1P
·P 𝐵)) |
39 | 6 | simp2d 1005 |
. . . . . . . 8
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝐵 ∈ P) |
40 | | mulassprg 7543 |
. . . . . . . 8
⊢ ((𝑦 ∈ P ∧
𝐶 ∈ P
∧ 𝐵 ∈
P) → ((𝑦
·P 𝐶) ·P 𝐵) = (𝑦 ·P (𝐶
·P 𝐵))) |
41 | 8, 16, 39, 40 | syl3anc 1233 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → ((𝑦 ·P 𝐶)
·P 𝐵) = (𝑦 ·P (𝐶
·P 𝐵))) |
42 | | mulcomprg 7542 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ P ∧
1P ∈ P) → (𝐵 ·P
1P) = (1P
·P 𝐵)) |
43 | 29, 42 | mpan2 423 |
. . . . . . . . 9
⊢ (𝐵 ∈ P →
(𝐵
·P 1P) =
(1P ·P 𝐵)) |
44 | | 1idpr 7554 |
. . . . . . . . 9
⊢ (𝐵 ∈ P →
(𝐵
·P 1P) = 𝐵) |
45 | 43, 44 | eqtr3d 2205 |
. . . . . . . 8
⊢ (𝐵 ∈ P →
(1P ·P 𝐵) = 𝐵) |
46 | 39, 45 | syl 14 |
. . . . . . 7
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) →
(1P ·P 𝐵) = 𝐵) |
47 | 38, 41, 46 | 3eqtr3d 2211 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝑦 ·P (𝐶
·P 𝐵)) = 𝐵) |
48 | 15, 37, 47 | 3eqtr3d 2211 |
. . . . 5
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → (𝐴 +P (𝑦
·P 𝑥)) = 𝐵) |
49 | 13, 48 | breqtrd 4015 |
. . . 4
⊢
(((((𝐴 ∈
P ∧ 𝐵
∈ P ∧ 𝐶 ∈ P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) ∧
(𝑥 ∈ P
∧ ((𝐶
·P 𝐴) +P 𝑥) = (𝐶 ·P 𝐵))) → 𝐴<P 𝐵) |
50 | 5, 49 | rexlimddv 2592 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) ∧ (𝑦 ∈ P ∧ (𝐶
·P 𝑦) = 1P)) →
𝐴<P 𝐵) |
51 | 3, 50 | rexlimddv 2592 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) ∧ (𝐶
·P 𝐴)<P (𝐶
·P 𝐵)) → 𝐴<P 𝐵) |
52 | 51 | ex 114 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P
∧ 𝐶 ∈
P) → ((𝐶
·P 𝐴)<P (𝐶
·P 𝐵) → 𝐴<P 𝐵)) |