MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  perfectlem2 Structured version   Visualization version   GIF version

Theorem perfectlem2 25733
Description: Lemma for perfect 25734. (Contributed by Mario Carneiro, 17-May-2016.) Replace OLD theorem. (Revised by Wolf Lammen, 17-Sep-2020.)
Hypotheses
Ref Expression
perfectlem.1 (𝜑𝐴 ∈ ℕ)
perfectlem.2 (𝜑𝐵 ∈ ℕ)
perfectlem.3 (𝜑 → ¬ 2 ∥ 𝐵)
perfectlem.4 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
Assertion
Ref Expression
perfectlem2 (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Proof of Theorem perfectlem2
Dummy variables 𝑘 𝑛 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 perfectlem.2 . . . 4 (𝜑𝐵 ∈ ℕ)
2 1red 10630 . . . . 5 (𝜑 → 1 ∈ ℝ)
3 perfectlem.1 . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
4 perfectlem.3 . . . . . . . 8 (𝜑 → ¬ 2 ∥ 𝐵)
5 perfectlem.4 . . . . . . . 8 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
63, 1, 4, 5perfectlem1 25732 . . . . . . 7 (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
76simp3d 1136 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
87nnred 11641 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
91nnred 11641 . . . . 5 (𝜑𝐵 ∈ ℝ)
107nnge1d 11673 . . . . 5 (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
11 2cn 11700 . . . . . . . . . . 11 2 ∈ ℂ
12 exp1 13423 . . . . . . . . . . 11 (2 ∈ ℂ → (2↑1) = 2)
1311, 12ax-mp 5 . . . . . . . . . 10 (2↑1) = 2
14 df-2 11688 . . . . . . . . . 10 2 = (1 + 1)
1513, 14eqtri 2841 . . . . . . . . 9 (2↑1) = (1 + 1)
16 2re 11699 . . . . . . . . . . 11 2 ∈ ℝ
1716a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
18 1zzd 12001 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
193peano2nnd 11643 . . . . . . . . . . 11 (𝜑 → (𝐴 + 1) ∈ ℕ)
2019nnzd 12074 . . . . . . . . . 10 (𝜑 → (𝐴 + 1) ∈ ℤ)
21 1lt2 11796 . . . . . . . . . . 11 1 < 2
2221a1i 11 . . . . . . . . . 10 (𝜑 → 1 < 2)
23 1re 10629 . . . . . . . . . . . 12 1 ∈ ℝ
243nnrpd 12417 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
25 ltaddrp 12414 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → 1 < (1 + 𝐴))
2623, 24, 25sylancr 587 . . . . . . . . . . 11 (𝜑 → 1 < (1 + 𝐴))
27 ax-1cn 10583 . . . . . . . . . . . 12 1 ∈ ℂ
283nncnd 11642 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
29 addcom 10814 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
3027, 28, 29sylancr 587 . . . . . . . . . . 11 (𝜑 → (1 + 𝐴) = (𝐴 + 1))
3126, 30breqtrd 5083 . . . . . . . . . 10 (𝜑 → 1 < (𝐴 + 1))
32 ltexp2a 13518 . . . . . . . . . 10 (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
3317, 18, 20, 22, 31, 32syl32anc 1370 . . . . . . . . 9 (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
3415, 33eqbrtrrid 5093 . . . . . . . 8 (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
356simp1d 1134 . . . . . . . . . 10 (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
3635nnred 11641 . . . . . . . . 9 (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
372, 2, 36ltaddsubd 11228 . . . . . . . 8 (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
3834, 37mpbid 233 . . . . . . 7 (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39 0lt1 11150 . . . . . . . . 9 0 < 1
4039a1i 11 . . . . . . . 8 (𝜑 → 0 < 1)
41 peano2rem 10941 . . . . . . . . 9 ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
4236, 41syl 17 . . . . . . . 8 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43 expgt1 13455 . . . . . . . . . 10 ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
4416, 19, 22, 43mp3an2i 1457 . . . . . . . . 9 (𝜑 → 1 < (2↑(𝐴 + 1)))
45 posdif 11121 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (2↑(𝐴 + 1)) ∈ ℝ) → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
4623, 36, 45sylancr 587 . . . . . . . . 9 (𝜑 → (1 < (2↑(𝐴 + 1)) ↔ 0 < ((2↑(𝐴 + 1)) − 1)))
4744, 46mpbid 233 . . . . . . . 8 (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
481nngt0d 11674 . . . . . . . 8 (𝜑 → 0 < 𝐵)
49 ltdiv2 11514 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 < 1) ∧ (((2↑(𝐴 + 1)) − 1) ∈ ℝ ∧ 0 < ((2↑(𝐴 + 1)) − 1)) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
502, 40, 42, 47, 9, 48, 49syl222anc 1378 . . . . . . 7 (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
5138, 50mpbid 233 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
521nncnd 11642 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
5352div1d 11396 . . . . . 6 (𝜑 → (𝐵 / 1) = 𝐵)
5451, 53breqtrd 5083 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
552, 8, 9, 10, 54lelttrd 10786 . . . 4 (𝜑 → 1 < 𝐵)
56 eluz2b2 12309 . . . 4 (𝐵 ∈ (ℤ‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
571, 55, 56sylanbrc 583 . . 3 (𝜑𝐵 ∈ (ℤ‘2))
58 fzfid 13329 . . . . . . . . . . . 12 (𝜑 → (1...𝐵) ∈ Fin)
59 dvdsssfz1 15656 . . . . . . . . . . . . 13 (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
601, 59syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
6158, 60ssfid 8729 . . . . . . . . . . 11 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
6261ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
63 ssrab2 4053 . . . . . . . . . . . . 13 {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ
6463a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ)
6564sselda 3964 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
6665nnred 11641 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
6765nnnn0d 11943 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
6867nn0ge0d 11946 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
69 df-tp 4562 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
707, 1prssd 4747 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
7170ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
72 simplrl 773 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
7372snssd 4734 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
7471, 73unssd 4159 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
7569, 74eqsstrid 4012 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
766simp2d 1135 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
7776nnzd 12074 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
787nnzd 12074 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
79 dvdsmul2 15620 . . . . . . . . . . . . . . . . 17 ((((2↑(𝐴 + 1)) − 1) ∈ ℤ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
8077, 78, 79syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
8176nncnd 11642 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
8276nnne0d 11675 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠ 0)
8352, 81, 82divcan2d 11406 . . . . . . . . . . . . . . . 16 (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
8480, 83breqtrd 5083 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
85 breq1 5060 . . . . . . . . . . . . . . 15 (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
8684, 85syl5ibrcom 248 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
8786ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
881nnzd 12074 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℤ)
89 iddvds 15611 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → 𝐵𝐵)
9088, 89syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐵)
91 breq1 5060 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (𝑥𝐵𝐵𝐵))
9290, 91syl5ibrcom 248 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 = 𝐵𝑥𝐵))
9392ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵𝑥𝐵))
94 simplrr 774 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛𝐵)
95 breq1 5060 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (𝑥𝐵𝑛𝐵))
9694, 95syl5ibrcom 248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛𝑥𝐵))
9787, 93, 963jaod 1420 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛) → 𝑥𝐵))
98 eltpi 4617 . . . . . . . . . . . 12 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛))
9997, 98impel 506 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥𝐵)
10075, 99ssrabdv 4047 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
10162, 66, 68, 100fsumless 15139 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
102 simpr 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
103 disjsn 4639 . . . . . . . . . . . 12 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
104102, 103sylibr 235 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
10569a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
106 tpfi 8782 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin
107106a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
10875sselda 3964 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
109108nncnd 11642 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
110104, 105, 107, 109fsumsplit 15085 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
1117nncnd 11642 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
112 id 22 . . . . . . . . . . . . . . . 16 (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
113112sumsn 15089 . . . . . . . . . . . . . . 15 (((𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
1147, 111, 113syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
115 id 22 . . . . . . . . . . . . . . . 16 (𝑘 = 𝐵𝑘 = 𝐵)
116115sumsn 15089 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
1171, 52, 116syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
118114, 117oveq12d 7163 . . . . . . . . . . . . 13 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
119 incom 4175 . . . . . . . . . . . . . . 15 ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
1208, 54gtned 10763 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
121 disjsn2 4640 . . . . . . . . . . . . . . . 16 (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
123119, 122syl5eqr 2867 . . . . . . . . . . . . . 14 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
124 df-pr 4560 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
125124a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
126 prfi 8781 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin
127126a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
12870sselda 3964 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
129128nncnd 11642 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
130123, 125, 127, 129fsumsplit 15085 . . . . . . . . . . . . 13 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
13181, 52mulcld 10649 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
13252, 131, 81, 82divdird 11442 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
13335nncnd 11642 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
134 1cnd 10624 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℂ)
135133, 134, 52subdird 11085 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
13652mulid2d 10647 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝐵) = 𝐵)
137136oveq2d 7161 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
138135, 137eqtrd 2853 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
139138oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
140133, 52mulcld 10649 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
14152, 140pncan3d 10988 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
142139, 141eqtrd 2853 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
143142oveq1d 7160 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
144133, 52, 81, 82divassd 11439 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
145143, 144eqtrd 2853 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
14652, 81, 82divcan3d 11409 . . . . . . . . . . . . . . 15 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
147146oveq2d 7161 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
148132, 145, 1473eqtr3d 2861 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
149118, 130, 1483eqtr4d 2863 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
150149ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
15172nncnd 11642 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
152 id 22 . . . . . . . . . . . . 13 (𝑘 = 𝑛𝑘 = 𝑛)
153152sumsn 15089 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
154151, 151, 153syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
155150, 154oveq12d 7163 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
156110, 155eqtrd 2853 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
1573nnnn0d 11943 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℕ0)
158 expp1 13424 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
15911, 157, 158sylancr 587 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
160 2nn 11698 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ
161 nnexpcl 13430 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ0) → (2↑𝐴) ∈ ℕ)
162160, 157, 161sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑𝐴) ∈ ℕ)
163162nncnd 11642 . . . . . . . . . . . . . . . . 17 (𝜑 → (2↑𝐴) ∈ ℂ)
164 mulcom 10611 . . . . . . . . . . . . . . . . 17 (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
165163, 11, 164sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
166159, 165eqtrd 2853 . . . . . . . . . . . . . . 15 (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
167166oveq1d 7160 . . . . . . . . . . . . . 14 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
168 2cnd 11703 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
169168, 163, 52mulassd 10652 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
170 2prm 16024 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℙ
171 coprm 16043 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℙ ∧ 𝐵 ∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
172170, 88, 171sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
1734, 172mpbid 233 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 gcd 𝐵) = 1)
174 2z 12002 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
175 rpexp1i 16053 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
176174, 88, 157, 175mp3an2i 1457 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
177173, 176mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
178 sgmmul 25704 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
179134, 162, 1, 177, 178syl13anc 1364 . . . . . . . . . . . . . . 15 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
180 pncan 10880 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
18128, 27, 180sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
182181oveq2d 7161 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
183182oveq2d 7161 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
184 1sgm2ppw 25703 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
18519, 184syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
186183, 185eqtr3d 2855 . . . . . . . . . . . . . . . 16 (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
187186oveq1d 7160 . . . . . . . . . . . . . . 15 (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
188179, 5, 1873eqtr3d 2861 . . . . . . . . . . . . . 14 (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
189167, 169, 1883eqtrd 2857 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
190189oveq1d 7160 . . . . . . . . . . . 12 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
191 1nn0 11901 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
192 sgmnncl 25651 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
193191, 1, 192sylancr 587 . . . . . . . . . . . . . 14 (𝜑 → (1 σ 𝐵) ∈ ℕ)
194193nncnd 11642 . . . . . . . . . . . . 13 (𝜑 → (1 σ 𝐵) ∈ ℂ)
195194, 81, 82divcan3d 11409 . . . . . . . . . . . 12 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
196190, 144, 1953eqtr3d 2861 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
197 sgmval 25646 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
19827, 1, 197sylancr 587 . . . . . . . . . . 11 (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
199 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
20063, 199sseldi 3962 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
201200nncnd 11642 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℂ)
202201cxp1d 25216 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → (𝑘𝑐1) = 𝑘)
203202sumeq2dv 15048 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
204196, 198, 2033eqtrrd 2858 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
205204ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
206101, 156, 2053brtr3d 5088 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
20736, 8remulcld 10659 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
208207ad2antrr 722 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
20972nnrpd 12417 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ+)
210208, 209ltaddrpd 12452 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
21172nnred 11641 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ)
212208, 211readdcld 10658 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ)
213208, 212ltnled 10775 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
214210, 213mpbid 233 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
215206, 214condan 814 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
216 elpri 4579 . . . . . . 7 (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
217215, 216syl 17 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
218217expr 457 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
219218ralrimiva 3179 . . . 4 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
2202, 55gtned 10763 . . . . . . . . . 10 (𝜑𝐵 ≠ 1)
221220necomd 3068 . . . . . . . . 9 (𝜑 → 1 ≠ 𝐵)
222 1dvds 15612 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → 1 ∥ 𝐵)
22388, 222syl 17 . . . . . . . . . . . 12 (𝜑 → 1 ∥ 𝐵)
224 breq1 5060 . . . . . . . . . . . . . 14 (𝑛 = 1 → (𝑛𝐵 ↔ 1 ∥ 𝐵))
225 eqeq1 2822 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
226 eqeq1 2822 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
227225, 226orbi12d 912 . . . . . . . . . . . . . 14 (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
228224, 227imbi12d 346 . . . . . . . . . . . . 13 (𝑛 = 1 → ((𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
229 1nn 11637 . . . . . . . . . . . . . 14 1 ∈ ℕ
230229a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℕ)
231228, 219, 230rspcdva 3622 . . . . . . . . . . . 12 (𝜑 → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
232223, 231mpd 15 . . . . . . . . . . 11 (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
233232ord 858 . . . . . . . . . 10 (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵))
234233necon1ad 3030 . . . . . . . . 9 (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
235221, 234mpd 15 . . . . . . . 8 (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
236235eqeq2d 2829 . . . . . . 7 (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
237236orbi1d 910 . . . . . 6 (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
238237imbi2d 342 . . . . 5 (𝜑 → ((𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
239238ralbidv 3194 . . . 4 (𝜑 → (∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
240219, 239mpbird 258 . . 3 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
241 isprm2 16014 . . 3 (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ‘2) ∧ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
24257, 240, 241sylanbrc 583 . 2 (𝜑𝐵 ∈ ℙ)
243207ltp1d 11558 . . . 4 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
244 peano2re 10801 . . . . . 6 (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
245207, 244syl 17 . . . . 5 (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
246207, 245ltnled 10775 . . . 4 (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ↔ ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
247243, 246mpbid 233 . . 3 (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
248200nnred 11641 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
249200nnnn0d 11943 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
250249nn0ge0d 11946 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
251 df-tp 4562 . . . . . . . . . 10 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
252 snssi 4733 . . . . . . . . . . . 12 (1 ∈ ℕ → {1} ⊆ ℕ)
253229, 252mp1i 13 . . . . . . . . . . 11 (𝜑 → {1} ⊆ ℕ)
25470, 253unssd 4159 . . . . . . . . . 10 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
255251, 254eqsstrid 4012 . . . . . . . . 9 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
256 breq1 5060 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥𝐵 ↔ 1 ∥ 𝐵))
257223, 256syl5ibrcom 248 . . . . . . . . . . 11 (𝜑 → (𝑥 = 1 → 𝑥𝐵))
25886, 92, 2573jaod 1420 . . . . . . . . . 10 (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1) → 𝑥𝐵))
259 eltpi 4617 . . . . . . . . . 10 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1))
260258, 259impel 506 . . . . . . . . 9 ((𝜑𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥𝐵)
261255, 260ssrabdv 4047 . . . . . . . 8 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
26261, 248, 250, 261fsumless 15139 . . . . . . 7 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
263262adantr 481 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
26452, 81, 82diveq1ad 11413 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
265264necon3bid 3057 . . . . . . . . . . . 12 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
266265biimpar 478 . . . . . . . . . . 11 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
267266necomd 3068 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
268221adantr 481 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
269267, 268nelprd 4586 . . . . . . . . 9 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
270 disjsn 4639 . . . . . . . . 9 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
271269, 270sylibr 235 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
272251a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
273 tpfi 8782 . . . . . . . . 9 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin
274273a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
275255adantr 481 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
276275sselda 3964 . . . . . . . . 9 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
277276nncnd 11642 . . . . . . . 8 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
278271, 272, 274, 277fsumsplit 15085 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
279 id 22 . . . . . . . . . . 11 (𝑘 = 1 → 𝑘 = 1)
280279sumsn 15089 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
2812, 27, 280sylancl 586 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
282149, 281oveq12d 7163 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
283282adantr 481 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
284278, 283eqtrd 2853 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
285204adantr 481 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
286263, 284, 2853brtr3d 5088 . . . . 5 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
287286ex 413 . . . 4 (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
288287necon1bd 3031 . . 3 (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1)))
289247, 288mpd 15 . 2 (𝜑𝐵 = ((2↑(𝐴 + 1)) − 1))
290242, 289jca 512 1 (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3o 1078   = wceq 1528  wcel 2105  wne 3013  wral 3135  {crab 3139  cun 3931  cin 3932  wss 3933  c0 4288  {csn 4557  {cpr 4559  {ctp 4561   class class class wbr 5057  cfv 6348  (class class class)co 7145  Fincfn 8497  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  cn 11626  2c2 11680  0cn0 11885  cz 11969  cuz 12231  +crp 12377  ...cfz 12880  cexp 13417  Σcsu 15030  cdvds 15595   gcd cgcd 15831  cprime 16003  𝑐ccxp 25066   σ csgm 25600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-fac 13622  df-bc 13651  df-hash 13679  df-shft 14414  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-ef 15409  df-sin 15411  df-cos 15412  df-pi 15414  df-dvds 15596  df-gcd 15832  df-prm 16004  df-pc 16162  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-limc 24391  df-dv 24392  df-log 25067  df-cxp 25068  df-sgm 25606
This theorem is referenced by:  perfect  25734
  Copyright terms: Public domain W3C validator