Proof of Theorem remulscllem1
Step | Hyp | Ref
| Expression |
1 | | oveq2 7428 |
. . . . . . 7
⊢ (𝑛 = (𝑝 ·s 𝑞) → ( 1s /su
𝑛) = ( 1s
/su (𝑝
·s 𝑞))) |
2 | 1 | oveq2d 7436 |
. . . . . 6
⊢ (𝑛 = (𝑝 ·s 𝑞) → (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞)))) |
3 | 2 | eqeq2d 2739 |
. . . . 5
⊢ (𝑛 = (𝑝 ·s 𝑞) → ((𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)) ↔ (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞))))) |
4 | | nnmulscl 28212 |
. . . . 5
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝑝 ·s 𝑞) ∈
ℕs) |
5 | | 1sno 27759 |
. . . . . . . . 9
⊢
1s ∈ No |
6 | 5 | a1i 11 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 1s ∈ No
) |
7 | | nnsno 28195 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℕs
→ 𝑝 ∈ No ) |
8 | 7 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑝 ∈ No
) |
9 | | nnsno 28195 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℕs
→ 𝑞 ∈ No ) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑞 ∈ No
) |
11 | | nnne0s 28204 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℕs
→ 𝑝 ≠ 0s
) |
12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑝 ≠ 0s ) |
13 | | nnne0s 28204 |
. . . . . . . . 9
⊢ (𝑞 ∈ ℕs
→ 𝑞 ≠ 0s
) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → 𝑞 ≠ 0s ) |
15 | 6, 8, 6, 10, 12, 14 | divmuldivsd 28129 |
. . . . . . 7
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (( 1s /su 𝑝) ·s (
1s /su 𝑞)) = (( 1s ·s
1s ) /su (𝑝 ·s 𝑞))) |
16 | | mulsrid 28012 |
. . . . . . . . 9
⊢ (
1s ∈ No → ( 1s
·s 1s ) = 1s ) |
17 | 5, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (
1s ·s 1s ) =
1s |
18 | 17 | oveq1i 7430 |
. . . . . . 7
⊢ ((
1s ·s 1s ) /su (𝑝 ·s 𝑞)) = ( 1s
/su (𝑝
·s 𝑞)) |
19 | 15, 18 | eqtrdi 2784 |
. . . . . 6
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (( 1s /su 𝑝) ·s (
1s /su 𝑞)) = ( 1s /su
(𝑝 ·s
𝑞))) |
20 | 19 | oveq2d 7436 |
. . . . 5
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su (𝑝 ·s 𝑞)))) |
21 | 3, 4, 20 | rspcedvdw 3612 |
. . . 4
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → ∃𝑛 ∈ ℕs (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛))) |
22 | | eqeq1 2732 |
. . . . 5
⊢ (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → (𝐴 = (𝐵𝐹( 1s /su 𝑛)) ↔ (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)))) |
23 | 22 | rexbidv 3175 |
. . . 4
⊢ (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → (∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)) ↔ ∃𝑛 ∈ ℕs
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹( 1s /su 𝑛)))) |
24 | 21, 23 | syl5ibrcom 246 |
. . 3
⊢ ((𝑝 ∈ ℕs
∧ 𝑞 ∈
ℕs) → (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛)))) |
25 | 24 | rexlimivv 3196 |
. 2
⊢
(∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) → ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛))) |
26 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 1s ∈ No ) |
27 | | nnsno 28195 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 𝑛 ∈ No ) |
28 | | nnne0s 28204 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕs
→ 𝑛 ≠ 0s
) |
29 | 26, 27, 28 | divscld 28121 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) ∈ No
) |
30 | 29 | mulsridd 28013 |
. . . . . . 7
⊢ (𝑛 ∈ ℕs
→ (( 1s /su 𝑛) ·s 1s ) = (
1s /su 𝑛)) |
31 | 30 | eqcomd 2734 |
. . . . . 6
⊢ (𝑛 ∈ ℕs
→ ( 1s /su 𝑛) = (( 1s /su 𝑛) ·s
1s )) |
32 | 31 | oveq2d 7436 |
. . . . 5
⊢ (𝑛 ∈ ℕs
→ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) |
33 | | 1nns 28214 |
. . . . . 6
⊢
1s ∈ ℕs |
34 | | oveq2 7428 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑛 → ( 1s /su
𝑝) = ( 1s
/su 𝑛)) |
35 | 34 | oveq1d 7435 |
. . . . . . . . 9
⊢ (𝑝 = 𝑛 → (( 1s /su
𝑝) ·s (
1s /su 𝑞)) = (( 1s /su
𝑛) ·s (
1s /su 𝑞))) |
36 | 35 | oveq2d 7436 |
. . . . . . . 8
⊢ (𝑝 = 𝑛 → (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞)))) |
37 | 36 | eqeq2d 2739 |
. . . . . . 7
⊢ (𝑝 = 𝑛 → ((𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))))) |
38 | | oveq2 7428 |
. . . . . . . . . . 11
⊢ (𝑞 = 1s → (
1s /su 𝑞) = ( 1s /su
1s )) |
39 | | divs1 28102 |
. . . . . . . . . . . 12
⊢ (
1s ∈ No → ( 1s
/su 1s ) = 1s ) |
40 | 5, 39 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (
1s /su 1s ) =
1s |
41 | 38, 40 | eqtrdi 2784 |
. . . . . . . . . 10
⊢ (𝑞 = 1s → (
1s /su 𝑞) = 1s ) |
42 | 41 | oveq2d 7436 |
. . . . . . . . 9
⊢ (𝑞 = 1s → ((
1s /su 𝑛) ·s ( 1s
/su 𝑞)) = ((
1s /su 𝑛) ·s 1s
)) |
43 | 42 | oveq2d 7436 |
. . . . . . . 8
⊢ (𝑞 = 1s → (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) |
44 | 43 | eqeq2d 2739 |
. . . . . . 7
⊢ (𝑞 = 1s → ((𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s )))) |
45 | 37, 44 | rspc2ev 3622 |
. . . . . 6
⊢ ((𝑛 ∈ ℕs
∧ 1s ∈ ℕs ∧ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) → ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
46 | 33, 45 | mp3an2 1446 |
. . . . 5
⊢ ((𝑛 ∈ ℕs
∧ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑛) ·s
1s ))) → ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
47 | 32, 46 | mpdan 686 |
. . . 4
⊢ (𝑛 ∈ ℕs
→ ∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
48 | | eqeq1 2732 |
. . . . 5
⊢ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → (𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ (𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
49 | 48 | 2rexbidv 3216 |
. . . 4
⊢ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → (∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ ∃𝑝 ∈ ℕs ∃𝑞 ∈ ℕs
(𝐵𝐹( 1s /su 𝑛)) = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
50 | 47, 49 | syl5ibrcom 246 |
. . 3
⊢ (𝑛 ∈ ℕs
→ (𝐴 = (𝐵𝐹( 1s /su 𝑛)) → ∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))))) |
51 | 50 | rexlimiv 3145 |
. 2
⊢
(∃𝑛 ∈
ℕs 𝐴 =
(𝐵𝐹( 1s /su 𝑛)) → ∃𝑝 ∈ ℕs
∃𝑞 ∈
ℕs 𝐴 =
(𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞)))) |
52 | 25, 51 | impbii 208 |
1
⊢
(∃𝑝 ∈
ℕs ∃𝑞 ∈ ℕs 𝐴 = (𝐵𝐹(( 1s /su 𝑝) ·s (
1s /su 𝑞))) ↔ ∃𝑛 ∈ ℕs 𝐴 = (𝐵𝐹( 1s /su 𝑛))) |