Proof of Theorem halfnq
| Step | Hyp | Ref
| Expression |
| 1 | | distrnq 11001 |
. . . 4
⊢ (𝐴
·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) = ((𝐴
·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) |
| 2 | | distrnq 11001 |
. . . . . . . 8
⊢
((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) =
(((1Q +Q
1Q) ·Q
(*Q‘(1Q
+Q 1Q)))
+Q ((1Q
+Q 1Q)
·Q
(*Q‘(1Q
+Q 1Q)))) |
| 3 | | 1nq 10968 |
. . . . . . . . . . 11
⊢
1Q ∈ Q |
| 4 | | addclnq 10985 |
. . . . . . . . . . 11
⊢
((1Q ∈ Q ∧
1Q ∈ Q) →
(1Q +Q
1Q) ∈ Q) |
| 5 | 3, 3, 4 | mp2an 692 |
. . . . . . . . . 10
⊢
(1Q +Q
1Q) ∈ Q |
| 6 | | recidnq 11005 |
. . . . . . . . . 10
⊢
((1Q +Q
1Q) ∈ Q →
((1Q +Q
1Q) ·Q
(*Q‘(1Q
+Q 1Q))) =
1Q) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢
((1Q +Q
1Q) ·Q
(*Q‘(1Q
+Q 1Q))) =
1Q |
| 8 | 7, 7 | oveq12i 7443 |
. . . . . . . 8
⊢
(((1Q +Q
1Q) ·Q
(*Q‘(1Q
+Q 1Q)))
+Q ((1Q
+Q 1Q)
·Q
(*Q‘(1Q
+Q 1Q)))) =
(1Q +Q
1Q) |
| 9 | 2, 8 | eqtri 2765 |
. . . . . . 7
⊢
((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) =
(1Q +Q
1Q) |
| 10 | 9 | oveq1i 7441 |
. . . . . 6
⊢
(((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))))
·Q
(*Q‘(1Q
+Q 1Q))) =
((1Q +Q
1Q) ·Q
(*Q‘(1Q
+Q 1Q))) |
| 11 | 7 | oveq2i 7442 |
. . . . . . 7
⊢
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q ((1Q
+Q 1Q)
·Q
(*Q‘(1Q
+Q 1Q)))) =
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q
1Q) |
| 12 | | mulassnq 10999 |
. . . . . . . 8
⊢
((((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q (1Q
+Q 1Q))
·Q
(*Q‘(1Q
+Q 1Q))) =
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q ((1Q
+Q 1Q)
·Q
(*Q‘(1Q
+Q 1Q)))) |
| 13 | | mulcomnq 10993 |
. . . . . . . . 9
⊢
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q (1Q
+Q 1Q)) =
((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) |
| 14 | 13 | oveq1i 7441 |
. . . . . . . 8
⊢
((((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q (1Q
+Q 1Q))
·Q
(*Q‘(1Q
+Q 1Q))) =
(((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))))
·Q
(*Q‘(1Q
+Q 1Q))) |
| 15 | 12, 14 | eqtr3i 2767 |
. . . . . . 7
⊢
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q ((1Q
+Q 1Q)
·Q
(*Q‘(1Q
+Q 1Q)))) =
(((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))))
·Q
(*Q‘(1Q
+Q 1Q))) |
| 16 | | recclnq 11006 |
. . . . . . . . 9
⊢
((1Q +Q
1Q) ∈ Q →
(*Q‘(1Q
+Q 1Q)) ∈
Q) |
| 17 | | addclnq 10985 |
. . . . . . . . 9
⊢
(((*Q‘(1Q
+Q 1Q)) ∈
Q ∧
(*Q‘(1Q
+Q 1Q)) ∈
Q) →
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) ∈
Q) |
| 18 | 16, 16, 17 | syl2anc 584 |
. . . . . . . 8
⊢
((1Q +Q
1Q) ∈ Q →
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) ∈
Q) |
| 19 | | mulidnq 11003 |
. . . . . . . 8
⊢
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) ∈
Q →
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q 1Q) =
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) |
| 20 | 5, 18, 19 | mp2b 10 |
. . . . . . 7
⊢
(((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))
·Q 1Q) =
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) |
| 21 | 11, 15, 20 | 3eqtr3i 2773 |
. . . . . 6
⊢
(((1Q +Q
1Q) ·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))))
·Q
(*Q‘(1Q
+Q 1Q))) =
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) |
| 22 | 10, 21, 7 | 3eqtr3i 2773 |
. . . . 5
⊢
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q))) =
1Q |
| 23 | 22 | oveq2i 7442 |
. . . 4
⊢ (𝐴
·Q
((*Q‘(1Q
+Q 1Q))
+Q
(*Q‘(1Q
+Q 1Q)))) = (𝐴
·Q
1Q) |
| 24 | 1, 23 | eqtr3i 2767 |
. . 3
⊢ ((𝐴
·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) = (𝐴
·Q
1Q) |
| 25 | | mulidnq 11003 |
. . 3
⊢ (𝐴 ∈ Q →
(𝐴
·Q 1Q) = 𝐴) |
| 26 | 24, 25 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈ Q →
((𝐴
·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) = 𝐴) |
| 27 | | ovex 7464 |
. . 3
⊢ (𝐴
·Q
(*Q‘(1Q
+Q 1Q))) ∈
V |
| 28 | | oveq12 7440 |
. . . . 5
⊢ ((𝑥 = (𝐴 ·Q
(*Q‘(1Q
+Q 1Q))) ∧ 𝑥 = (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) → (𝑥 +Q
𝑥) = ((𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q))))) |
| 29 | 28 | anidms 566 |
. . . 4
⊢ (𝑥 = (𝐴 ·Q
(*Q‘(1Q
+Q 1Q))) → (𝑥 +Q
𝑥) = ((𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q))))) |
| 30 | 29 | eqeq1d 2739 |
. . 3
⊢ (𝑥 = (𝐴 ·Q
(*Q‘(1Q
+Q 1Q))) → ((𝑥 +Q
𝑥) = 𝐴 ↔ ((𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) = 𝐴)) |
| 31 | 27, 30 | spcev 3606 |
. 2
⊢ (((𝐴
·Q
(*Q‘(1Q
+Q 1Q)))
+Q (𝐴 ·Q
(*Q‘(1Q
+Q 1Q)))) = 𝐴 → ∃𝑥(𝑥 +Q 𝑥) = 𝐴) |
| 32 | 26, 31 | syl 17 |
1
⊢ (𝐴 ∈ Q →
∃𝑥(𝑥 +Q 𝑥) = 𝐴) |