Proof of Theorem remulscllem1
| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑛 = (𝑝 ·s 𝑞) → ( 1s /su
𝑛) = ( 1s
/su (𝑝
·s 𝑞))) |
| 2 | 1 | oveq2d 7447 |
. . . . . 6
⊢ (𝑛 = (𝑝 ·s 𝑞) → (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞)))) |
| 3 | 2 | eqeq2d 2748 |
. . . . 5
⊢ (𝑛 = (𝑝 ·s 𝑞) → ((𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)) ↔ (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞))))) |
| 4 | | nnmulscl 28350 |
. . . . 5
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝑝 ·s 𝑞) ∈
ℕs) |
| 5 | | 1sno 27872 |
. . . . . . . . 9
⊢
1s ∈ No |
| 6 | 5 | a1i 11 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 1s ∈ No
) |
| 7 | | nnsno 28329 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℕs
→ 𝑝 ∈ No ) |
| 8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑝 ∈ No
) |
| 9 | | nnsno 28329 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℕs
→ 𝑞 ∈ No ) |
| 10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑞 ∈ No
) |
| 11 | | nnne0s 28340 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℕs
→ 𝑝 ≠ 0s
) |
| 12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑝 ≠ 0s ) |
| 13 | | nnne0s 28340 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℕs
→ 𝑞 ≠ 0s
) |
| 14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑞 ≠ 0s ) |
| 15 | 6, 8, 6, 10, 12, 14 | divmuldivsd 28256 |
. . . . . . 7
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (( 1s /su 𝑝) ·s (
1s /su 𝑞)) = (( 1s ·s
1s ) /su (𝑝 ·s 𝑞))) |
| 16 | | mulsrid 28139 |
. . . . . . . . 9
⊢ (
1s ∈ No → ( 1s
·s 1s ) = 1s ) |
| 17 | 5, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (
1s ·s 1s ) =
1s |
| 18 | 17 | oveq1i 7441 |
. . . . . . 7
⊢ ((
1s ·s 1s ) /su (𝑝 ·s 𝑞)) = ( 1s
/su (𝑝
·s 𝑞)) |
| 19 | 15, 18 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (( 1s /su 𝑝) ·s (
1s /su 𝑞)) = ( 1s /su
(𝑝 ·s
𝑞))) |
| 20 | 19 | oveq2d 7447 |
. . . . 5
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞)))) |
| 21 | 3, 4, 20 | rspcedvdw 3625 |
. . . 4
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → ∃𝑛 ∈ ℕs (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛))) |
| 22 | | eqeq1 2741 |
. . . . 5
⊢ (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → (𝐴 = (𝐵𝐹( 1s /su 𝑛)) ↔ (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)))) |
| 23 | 22 | rexbidv 3179 |
. . . 4
⊢ (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → (∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)))) |
| 24 | 21, 23 | syl5ibrcom 247 |
. . 3
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)))) |
| 25 | 24 | rexlimivv 3201 |
. 2
⊢
(∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛))) |
| 26 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
| 27 | | nnsno 28329 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
| 28 | | nnne0s 28340 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
| 29 | 26, 27, 28 | divscld 28248 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
| 30 | 29 | mulsridd 28140 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (( 1s /su 𝑛) ·s 1s ) = (
1s /su 𝑛)) |
| 31 | 30 | eqcomd 2743 |
. . . . . 6
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) = (( 1s /su 𝑛) ·s
1s )) |
| 32 | 31 | oveq2d 7447 |
. . . . 5
⊢ (𝑛 ∈ ℕs
→ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) |
| 33 | | 1nns 28352 |
. . . . . 6
⊢
1s ∈ ℕs |
| 34 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑛 → ( 1s /su
𝑝) = ( 1s
/su 𝑛)) |
| 35 | 34 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝑝 = 𝑛 → (( 1s /su
𝑝) ·s (
1s /su 𝑞)) = (( 1s /su
𝑛) ·s (
1s /su 𝑞))) |
| 36 | 35 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑝 = 𝑛 → (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞)))) |
| 37 | 36 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑝 = 𝑛 → ((𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))))) |
| 38 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑞 = 1s → (
1s /su 𝑞) = ( 1s /su
1s )) |
| 39 | | divs1 28229 |
. . . . . . . . . . . 12
⊢ (
1s ∈ No → ( 1s
/su 1s ) = 1s ) |
| 40 | 5, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (
1s /su 1s ) =
1s |
| 41 | 38, 40 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑞 = 1s → (
1s /su 𝑞) = 1s ) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑞 = 1s → ((
1s /su 𝑛) ·s ( 1s
/su 𝑞)) = ((
1s /su 𝑛) ·s 1s
)) |
| 43 | 42 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑞 = 1s → (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) |
| 44 | 43 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑞 = 1s → ((𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s )))) |
| 45 | 37, 44 | rspc2ev 3635 |
. . . . . 6
⊢ ((𝑛 ∈ ℕs
∧ 1s ∈ ℕs ∧ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) → ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
| 46 | 33, 45 | mp3an2 1451 |
. . . . 5
⊢ ((𝑛 ∈ ℕs
∧ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) → ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
| 47 | 32, 46 | mpdan 687 |
. . . 4
⊢ (𝑛 ∈ ℕs
→ ∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
| 48 | | eqeq1 2741 |
. . . . 5
⊢ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
| 49 | 48 | 2rexbidv 3222 |
. . . 4
⊢ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → (∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
| 50 | 47, 49 | syl5ibrcom 247 |
. . 3
⊢ (𝑛 ∈ ℕs
→ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → ∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
| 51 | 50 | rexlimiv 3148 |
. 2
⊢
(∃𝑛 ∈
ℕs 𝐴 =
(𝐵𝐹( 1s /su 𝑛)) → ∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
| 52 | 25, 51 | impbii 209 |
1
⊢
(∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛))) |