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

Theorem perfectlem2 27274
Description: Lemma for perfect 27275. (Contributed by Mario Carneiro, 17-May-2016.) (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 11262 . . . . 5 (𝜑 → 1 ∈ ℝ)
3 perfectlem.1 . . . . . . . 8 (𝜑𝐴 ∈ ℕ)
4 perfectlem.3 . . . . . . . 8 (𝜑 → ¬ 2 ∥ 𝐵)
5 perfectlem.4 . . . . . . . 8 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))
63, 1, 4, 5perfectlem1 27273 . . . . . . 7 (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ))
76simp3d 1145 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)
87nnred 12281 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℝ)
91nnred 12281 . . . . 5 (𝜑𝐵 ∈ ℝ)
107nnge1d 12314 . . . . 5 (𝜑 → 1 ≤ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
11 2cn 12341 . . . . . . . . . . 11 2 ∈ ℂ
12 exp1 14108 . . . . . . . . . . 11 (2 ∈ ℂ → (2↑1) = 2)
1311, 12ax-mp 5 . . . . . . . . . 10 (2↑1) = 2
14 df-2 12329 . . . . . . . . . 10 2 = (1 + 1)
1513, 14eqtri 2765 . . . . . . . . 9 (2↑1) = (1 + 1)
16 2re 12340 . . . . . . . . . . 11 2 ∈ ℝ
1716a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℝ)
18 1zzd 12648 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
193peano2nnd 12283 . . . . . . . . . . 11 (𝜑 → (𝐴 + 1) ∈ ℕ)
2019nnzd 12640 . . . . . . . . . 10 (𝜑 → (𝐴 + 1) ∈ ℤ)
21 1lt2 12437 . . . . . . . . . . 11 1 < 2
2221a1i 11 . . . . . . . . . 10 (𝜑 → 1 < 2)
23 1re 11261 . . . . . . . . . . . 12 1 ∈ ℝ
243nnrpd 13075 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ+)
25 ltaddrp 13072 . . . . . . . . . . . 12 ((1 ∈ ℝ ∧ 𝐴 ∈ ℝ+) → 1 < (1 + 𝐴))
2623, 24, 25sylancr 587 . . . . . . . . . . 11 (𝜑 → 1 < (1 + 𝐴))
27 ax-1cn 11213 . . . . . . . . . . . 12 1 ∈ ℂ
283nncnd 12282 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℂ)
29 addcom 11447 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐴 ∈ ℂ) → (1 + 𝐴) = (𝐴 + 1))
3027, 28, 29sylancr 587 . . . . . . . . . . 11 (𝜑 → (1 + 𝐴) = (𝐴 + 1))
3126, 30breqtrd 5169 . . . . . . . . . 10 (𝜑 → 1 < (𝐴 + 1))
32 ltexp2a 14206 . . . . . . . . . 10 (((2 ∈ ℝ ∧ 1 ∈ ℤ ∧ (𝐴 + 1) ∈ ℤ) ∧ (1 < 2 ∧ 1 < (𝐴 + 1))) → (2↑1) < (2↑(𝐴 + 1)))
3317, 18, 20, 22, 31, 32syl32anc 1380 . . . . . . . . 9 (𝜑 → (2↑1) < (2↑(𝐴 + 1)))
3415, 33eqbrtrrid 5179 . . . . . . . 8 (𝜑 → (1 + 1) < (2↑(𝐴 + 1)))
356simp1d 1143 . . . . . . . . . 10 (𝜑 → (2↑(𝐴 + 1)) ∈ ℕ)
3635nnred 12281 . . . . . . . . 9 (𝜑 → (2↑(𝐴 + 1)) ∈ ℝ)
372, 2, 36ltaddsubd 11863 . . . . . . . 8 (𝜑 → ((1 + 1) < (2↑(𝐴 + 1)) ↔ 1 < ((2↑(𝐴 + 1)) − 1)))
3834, 37mpbid 232 . . . . . . 7 (𝜑 → 1 < ((2↑(𝐴 + 1)) − 1))
39 0lt1 11785 . . . . . . . . 9 0 < 1
4039a1i 11 . . . . . . . 8 (𝜑 → 0 < 1)
41 peano2rem 11576 . . . . . . . . 9 ((2↑(𝐴 + 1)) ∈ ℝ → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
4236, 41syl 17 . . . . . . . 8 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℝ)
43 expgt1 14141 . . . . . . . . . 10 ((2 ∈ ℝ ∧ (𝐴 + 1) ∈ ℕ ∧ 1 < 2) → 1 < (2↑(𝐴 + 1)))
4416, 19, 22, 43mp3an2i 1468 . . . . . . . . 9 (𝜑 → 1 < (2↑(𝐴 + 1)))
45 posdif 11756 . . . . . . . . . 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 232 . . . . . . . 8 (𝜑 → 0 < ((2↑(𝐴 + 1)) − 1))
481nngt0d 12315 . . . . . . . 8 (𝜑 → 0 < 𝐵)
49 ltdiv2 12154 . . . . . . . 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 1388 . . . . . . 7 (𝜑 → (1 < ((2↑(𝐴 + 1)) − 1) ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1)))
5138, 50mpbid 232 . . . . . 6 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < (𝐵 / 1))
521nncnd 12282 . . . . . . 7 (𝜑𝐵 ∈ ℂ)
5352div1d 12035 . . . . . 6 (𝜑 → (𝐵 / 1) = 𝐵)
5451, 53breqtrd 5169 . . . . 5 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) < 𝐵)
552, 8, 9, 10, 54lelttrd 11419 . . . 4 (𝜑 → 1 < 𝐵)
56 eluz2b2 12963 . . . 4 (𝐵 ∈ (ℤ‘2) ↔ (𝐵 ∈ ℕ ∧ 1 < 𝐵))
571, 55, 56sylanbrc 583 . . 3 (𝜑𝐵 ∈ (ℤ‘2))
58 fzfid 14014 . . . . . . . . . . . 12 (𝜑 → (1...𝐵) ∈ Fin)
59 dvdsssfz1 16355 . . . . . . . . . . . . 13 (𝐵 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
601, 59syl 17 . . . . . . . . . . . 12 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ (1...𝐵))
6158, 60ssfid 9301 . . . . . . . . . . 11 (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
6261ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ∈ Fin)
63 ssrab2 4080 . . . . . . . . . . . . 13 {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ
6463a1i 11 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑥 ∈ ℕ ∣ 𝑥𝐵} ⊆ ℕ)
6564sselda 3983 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
6665nnred 12281 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
6765nnnn0d 12587 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
6867nn0ge0d 12590 . . . . . . . . . 10 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
69 df-tp 4631 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛})
707, 1prssd 4822 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
7170ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ⊆ ℕ)
72 simplrl 777 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℕ)
7372snssd 4809 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {𝑛} ⊆ ℕ)
7471, 73unssd 4192 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}) ⊆ ℕ)
7569, 74eqsstrid 4022 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ ℕ)
766simp2d 1144 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℕ)
7776nnzd 12640 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℤ)
787nnzd 12640 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℤ)
79 dvdsmul2 16316 . . . . . . . . . . . . . . . . 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 12282 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ∈ ℂ)
8276nnne0d 12316 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2↑(𝐴 + 1)) − 1) ≠ 0)
8352, 81, 82divcan2d 12045 . . . . . . . . . . . . . . . 16 (𝜑 → (((2↑(𝐴 + 1)) − 1) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = 𝐵)
8480, 83breqtrd 5169 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵)
85 breq1 5146 . . . . . . . . . . . . . . 15 (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → (𝑥𝐵 ↔ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∥ 𝐵))
8684, 85syl5ibrcom 247 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
8786ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑥𝐵))
881nnzd 12640 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ∈ ℤ)
89 iddvds 16307 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℤ → 𝐵𝐵)
9088, 89syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵𝐵)
91 breq1 5146 . . . . . . . . . . . . . . 15 (𝑥 = 𝐵 → (𝑥𝐵𝐵𝐵))
9290, 91syl5ibrcom 247 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 = 𝐵𝑥𝐵))
9392ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝐵𝑥𝐵))
94 simplrr 778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛𝐵)
95 breq1 5146 . . . . . . . . . . . . . 14 (𝑥 = 𝑛 → (𝑥𝐵𝑛𝐵))
9694, 95syl5ibrcom 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (𝑥 = 𝑛𝑥𝐵))
9787, 93, 963jaod 1431 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛) → 𝑥𝐵))
98 eltpi 4688 . . . . . . . . . . . 12 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 𝑛))
9997, 98impel 505 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑥𝐵)
10075, 99ssrabdv 4074 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
10162, 66, 68, 100fsumless 15832 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
102 simpr 484 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
103 disjsn 4711 . . . . . . . . . . . 12 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
104102, 103sylibr 234 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {𝑛}) = ∅)
10569a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {𝑛}))
106 tpfi 9365 . . . . . . . . . . . 12 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin
107106a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛} ∈ Fin)
10875sselda 3983 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℕ)
109108nncnd 12282 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}) → 𝑘 ∈ ℂ)
110104, 105, 107, 109fsumsplit 15777 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘))
1117nncnd 12282 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℂ)
112 id 22 . . . . . . . . . . . . . . . 16 (𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 𝑘 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
113112sumsn 15782 . . . . . . . . . . . . . . 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 15782 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℕ ∧ 𝐵 ∈ ℂ) → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
1171, 52, 116syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → Σ𝑘 ∈ {𝐵}𝑘 = 𝐵)
118114, 117oveq12d 7449 . . . . . . . . . . . . 13 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
119 incom 4209 . . . . . . . . . . . . . . 15 ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵})
1208, 54gtned 11396 . . . . . . . . . . . . . . . 16 (𝜑𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
121 disjsn2 4712 . . . . . . . . . . . . . . . 16 (𝐵 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)) → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ({𝐵} ∩ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}) = ∅)
123119, 122eqtr3id 2791 . . . . . . . . . . . . . 14 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∩ {𝐵}) = ∅)
124 df-pr 4629 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵})
125124a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1))} ∪ {𝐵}))
126 prfi 9363 . . . . . . . . . . . . . . 15 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin
127126a1i 11 . . . . . . . . . . . . . 14 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∈ Fin)
12870sselda 3983 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℕ)
129128nncnd 12282 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑘 ∈ ℂ)
130123, 125, 127, 129fsumsplit 15777 . . . . . . . . . . . . 13 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1))}𝑘 + Σ𝑘 ∈ {𝐵}𝑘))
13181, 52mulcld 11281 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) ∈ ℂ)
13252, 131, 81, 82divdird 12081 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))))
13335nncnd 12282 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2↑(𝐴 + 1)) ∈ ℂ)
134 1cnd 11256 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 1 ∈ ℂ)
135133, 134, 52subdird 11720 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)))
13652mullidd 11279 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1 · 𝐵) = 𝐵)
137136oveq2d 7447 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) − (1 · 𝐵)) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
138135, 137eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2↑(𝐴 + 1)) − 1) · 𝐵) = (((2↑(𝐴 + 1)) · 𝐵) − 𝐵))
139138oveq2d 7447 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)))
140133, 52mulcld 11281 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) ∈ ℂ)
14152, 140pncan3d 11623 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) · 𝐵) − 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
142139, 141eqtrd 2777 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) = ((2↑(𝐴 + 1)) · 𝐵))
143142oveq1d 7446 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)))
144133, 52, 81, 82divassd 12078 . . . . . . . . . . . . . . 15 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
145143, 144eqtrd 2777 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 + (((2↑(𝐴 + 1)) − 1) · 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
14652, 81, 82divcan3d 12048 . . . . . . . . . . . . . . 15 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = 𝐵)
147146oveq2d 7447 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + ((((2↑(𝐴 + 1)) − 1) · 𝐵) / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
148132, 145, 1473eqtr3d 2785 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = ((𝐵 / ((2↑(𝐴 + 1)) − 1)) + 𝐵))
149118, 130, 1483eqtr4d 2787 . . . . . . . . . . . 12 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
150149ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
15172nncnd 12282 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℂ)
152 id 22 . . . . . . . . . . . . 13 (𝑘 = 𝑛𝑘 = 𝑛)
153152sumsn 15782 . . . . . . . . . . . 12 ((𝑛 ∈ ℂ ∧ 𝑛 ∈ ℂ) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
154151, 151, 153syl2anc 584 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑛}𝑘 = 𝑛)
155150, 154oveq12d 7449 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {𝑛}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
156110, 155eqtrd 2777 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 𝑛}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
1573nnnn0d 12587 . . . . . . . . . . . . . . . . 17 (𝜑𝐴 ∈ ℕ0)
158 expp1 14109 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℂ ∧ 𝐴 ∈ ℕ0) → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
15911, 157, 158sylancr 587 . . . . . . . . . . . . . . . 16 (𝜑 → (2↑(𝐴 + 1)) = ((2↑𝐴) · 2))
160 2nn 12339 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ
161 nnexpcl 14115 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℕ ∧ 𝐴 ∈ ℕ0) → (2↑𝐴) ∈ ℕ)
162160, 157, 161sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑𝐴) ∈ ℕ)
163162nncnd 12282 . . . . . . . . . . . . . . . . 17 (𝜑 → (2↑𝐴) ∈ ℂ)
164 mulcom 11241 . . . . . . . . . . . . . . . . 17 (((2↑𝐴) ∈ ℂ ∧ 2 ∈ ℂ) → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
165163, 11, 164sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) · 2) = (2 · (2↑𝐴)))
166159, 165eqtrd 2777 . . . . . . . . . . . . . . 15 (𝜑 → (2↑(𝐴 + 1)) = (2 · (2↑𝐴)))
167166oveq1d 7446 . . . . . . . . . . . . . 14 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = ((2 · (2↑𝐴)) · 𝐵))
168 2cnd 12344 . . . . . . . . . . . . . . 15 (𝜑 → 2 ∈ ℂ)
169168, 163, 52mulassd 11284 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (2↑𝐴)) · 𝐵) = (2 · ((2↑𝐴) · 𝐵)))
170 2prm 16729 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℙ
171 coprm 16748 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℙ ∧ 𝐵 ∈ ℤ) → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
172170, 88, 171sylancr 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 2 ∥ 𝐵 ↔ (2 gcd 𝐵) = 1))
1734, 172mpbid 232 . . . . . . . . . . . . . . . . 17 (𝜑 → (2 gcd 𝐵) = 1)
174 2z 12649 . . . . . . . . . . . . . . . . . 18 2 ∈ ℤ
175 rpexp1i 16760 . . . . . . . . . . . . . . . . . 18 ((2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
176174, 88, 157, 175mp3an2i 1468 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2 gcd 𝐵) = 1 → ((2↑𝐴) gcd 𝐵) = 1))
177173, 176mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ((2↑𝐴) gcd 𝐵) = 1)
178 sgmmul 27245 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ ((2↑𝐴) ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ((2↑𝐴) gcd 𝐵) = 1)) → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
179134, 162, 1, 177, 178syl13anc 1374 . . . . . . . . . . . . . . 15 (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = ((1 σ (2↑𝐴)) · (1 σ 𝐵)))
180 pncan 11514 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐴 + 1) − 1) = 𝐴)
18128, 27, 180sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐴 + 1) − 1) = 𝐴)
182181oveq2d 7447 . . . . . . . . . . . . . . . . . 18 (𝜑 → (2↑((𝐴 + 1) − 1)) = (2↑𝐴))
183182oveq2d 7447 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = (1 σ (2↑𝐴)))
184 1sgm2ppw 27244 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 1) ∈ ℕ → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
18519, 184syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 σ (2↑((𝐴 + 1) − 1))) = ((2↑(𝐴 + 1)) − 1))
186183, 185eqtr3d 2779 . . . . . . . . . . . . . . . 16 (𝜑 → (1 σ (2↑𝐴)) = ((2↑(𝐴 + 1)) − 1))
187186oveq1d 7446 . . . . . . . . . . . . . . 15 (𝜑 → ((1 σ (2↑𝐴)) · (1 σ 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
188179, 5, 1873eqtr3d 2785 . . . . . . . . . . . . . 14 (𝜑 → (2 · ((2↑𝐴) · 𝐵)) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
189167, 169, 1883eqtrd 2781 . . . . . . . . . . . . 13 (𝜑 → ((2↑(𝐴 + 1)) · 𝐵) = (((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)))
190189oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → (((2↑(𝐴 + 1)) · 𝐵) / ((2↑(𝐴 + 1)) − 1)) = ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)))
191 1nn0 12542 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
192 sgmnncl 27190 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝐵 ∈ ℕ) → (1 σ 𝐵) ∈ ℕ)
193191, 1, 192sylancr 587 . . . . . . . . . . . . . 14 (𝜑 → (1 σ 𝐵) ∈ ℕ)
194193nncnd 12282 . . . . . . . . . . . . 13 (𝜑 → (1 σ 𝐵) ∈ ℂ)
195194, 81, 82divcan3d 12048 . . . . . . . . . . . 12 (𝜑 → ((((2↑(𝐴 + 1)) − 1) · (1 σ 𝐵)) / ((2↑(𝐴 + 1)) − 1)) = (1 σ 𝐵))
196190, 144, 1953eqtr3d 2785 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) = (1 σ 𝐵))
197 sgmval 27185 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝐵 ∈ ℕ) → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
19827, 1, 197sylancr 587 . . . . . . . . . . 11 (𝜑 → (1 σ 𝐵) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1))
199 simpr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
20063, 199sselid 3981 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ)
201200nncnd 12282 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℂ)
202201cxp1d 26748 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → (𝑘𝑐1) = 𝑘)
203202sumeq2dv 15738 . . . . . . . . . . 11 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵} (𝑘𝑐1) = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
204196, 198, 2033eqtrrd 2782 . . . . . . . . . 10 (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
205204ad2antrr 726 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
206101, 156, 2053brtr3d 5174 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
20736, 8remulcld 11291 . . . . . . . . . . 11 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
208207ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ)
20972nnrpd 13075 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ+)
210208, 209ltaddrpd 13110 . . . . . . . . 9 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛))
21172nnred 12281 . . . . . . . . . . 11 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → 𝑛 ∈ ℝ)
212208, 211readdcld 11290 . . . . . . . . . 10 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ∈ ℝ)
213208, 212ltnled 11408 . . . . . . . . 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 232 . . . . . . . 8 (((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) ∧ ¬ 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}) → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 𝑛) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
215206, 214condan 818 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → 𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
216 elpri 4649 . . . . . . 7 (𝑛 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
217215, 216syl 17 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑛𝐵)) → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))
218217expr 456 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
219218ralrimiva 3146 . . . 4 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
2202, 55gtned 11396 . . . . . . . . . 10 (𝜑𝐵 ≠ 1)
221220necomd 2996 . . . . . . . . 9 (𝜑 → 1 ≠ 𝐵)
222 1dvds 16308 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → 1 ∥ 𝐵)
22388, 222syl 17 . . . . . . . . . . . 12 (𝜑 → 1 ∥ 𝐵)
224 breq1 5146 . . . . . . . . . . . . . 14 (𝑛 = 1 → (𝑛𝐵 ↔ 1 ∥ 𝐵))
225 eqeq1 2741 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ↔ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
226 eqeq1 2741 . . . . . . . . . . . . . . 15 (𝑛 = 1 → (𝑛 = 𝐵 ↔ 1 = 𝐵))
227225, 226orbi12d 919 . . . . . . . . . . . . . 14 (𝑛 = 1 → ((𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵) ↔ (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
228224, 227imbi12d 344 . . . . . . . . . . . . 13 (𝑛 = 1 → ((𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)) ↔ (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))))
229 1nn 12277 . . . . . . . . . . . . . 14 1 ∈ ℕ
230229a1i 11 . . . . . . . . . . . . 13 (𝜑 → 1 ∈ ℕ)
231228, 219, 230rspcdva 3623 . . . . . . . . . . . 12 (𝜑 → (1 ∥ 𝐵 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵)))
232223, 231mpd 15 . . . . . . . . . . 11 (𝜑 → (1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 1 = 𝐵))
233232ord 865 . . . . . . . . . 10 (𝜑 → (¬ 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) → 1 = 𝐵))
234233necon1ad 2957 . . . . . . . . 9 (𝜑 → (1 ≠ 𝐵 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
235221, 234mpd 15 . . . . . . . 8 (𝜑 → 1 = (𝐵 / ((2↑(𝐴 + 1)) − 1)))
236235eqeq2d 2748 . . . . . . 7 (𝜑 → (𝑛 = 1 ↔ 𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1))))
237236orbi1d 917 . . . . . 6 (𝜑 → ((𝑛 = 1 ∨ 𝑛 = 𝐵) ↔ (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵)))
238237imbi2d 340 . . . . 5 (𝜑 → ((𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
239238ralbidv 3178 . . . 4 (𝜑 → (∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)) ↔ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑛 = 𝐵))))
240219, 239mpbird 257 . . 3 (𝜑 → ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵)))
241 isprm2 16719 . . 3 (𝐵 ∈ ℙ ↔ (𝐵 ∈ (ℤ‘2) ∧ ∀𝑛 ∈ ℕ (𝑛𝐵 → (𝑛 = 1 ∨ 𝑛 = 𝐵))))
24257, 240, 241sylanbrc 583 . 2 (𝜑𝐵 ∈ ℙ)
243207ltp1d 12198 . . . 4 (𝜑 → ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) < (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
244 peano2re 11434 . . . . . 6 (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) ∈ ℝ → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
245207, 244syl 17 . . . . 5 (𝜑 → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ∈ ℝ)
246207, 245ltnled 11408 . . . 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 232 . . 3 (𝜑 → ¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
248200nnred 12281 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℝ)
249200nnnn0d 12587 . . . . . . . . 9 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 𝑘 ∈ ℕ0)
250249nn0ge0d 12590 . . . . . . . 8 ((𝜑𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}) → 0 ≤ 𝑘)
251 df-tp 4631 . . . . . . . . . 10 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1})
252 snssi 4808 . . . . . . . . . . . 12 (1 ∈ ℕ → {1} ⊆ ℕ)
253229, 252mp1i 13 . . . . . . . . . . 11 (𝜑 → {1} ⊆ ℕ)
25470, 253unssd 4192 . . . . . . . . . 10 (𝜑 → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}) ⊆ ℕ)
255251, 254eqsstrid 4022 . . . . . . . . 9 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
256 breq1 5146 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥𝐵 ↔ 1 ∥ 𝐵))
257223, 256syl5ibrcom 247 . . . . . . . . . . 11 (𝜑 → (𝑥 = 1 → 𝑥𝐵))
25886, 92, 2573jaod 1431 . . . . . . . . . 10 (𝜑 → ((𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1) → 𝑥𝐵))
259 eltpi 4688 . . . . . . . . . 10 (𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} → (𝑥 = (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∨ 𝑥 = 𝐵𝑥 = 1))
260258, 259impel 505 . . . . . . . . 9 ((𝜑𝑥 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑥𝐵)
261255, 260ssrabdv 4074 . . . . . . . 8 (𝜑 → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ {𝑥 ∈ ℕ ∣ 𝑥𝐵})
26261, 248, 250, 261fsumless 15832 . . . . . . 7 (𝜑 → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
263262adantr 480 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 ≤ Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘)
26452, 81, 82diveq1ad 12052 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) = 1 ↔ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
265264necon3bid 2985 . . . . . . . . . . . 12 (𝜑 → ((𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1 ↔ 𝐵 ≠ ((2↑(𝐴 + 1)) − 1)))
266265biimpar 477 . . . . . . . . . . 11 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (𝐵 / ((2↑(𝐴 + 1)) − 1)) ≠ 1)
267266necomd 2996 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ (𝐵 / ((2↑(𝐴 + 1)) − 1)))
268221adantr 480 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → 1 ≠ 𝐵)
269267, 268nelprd 4657 . . . . . . . . 9 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
270 disjsn 4711 . . . . . . . . 9 (({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅ ↔ ¬ 1 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵})
271269, 270sylibr 234 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∩ {1}) = ∅)
272251a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} = ({(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵} ∪ {1}))
273 tpfi 9365 . . . . . . . . 9 {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin
274273a1i 11 . . . . . . . 8 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ∈ Fin)
275255adantr 480 . . . . . . . . . 10 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1} ⊆ ℕ)
276275sselda 3983 . . . . . . . . 9 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℕ)
277276nncnd 12282 . . . . . . . 8 (((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) ∧ 𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}) → 𝑘 ∈ ℂ)
278271, 272, 274, 277fsumsplit 15777 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘))
279 id 22 . . . . . . . . . . 11 (𝑘 = 1 → 𝑘 = 1)
280279sumsn 15782 . . . . . . . . . 10 ((1 ∈ ℝ ∧ 1 ∈ ℂ) → Σ𝑘 ∈ {1}𝑘 = 1)
2812, 27, 280sylancl 586 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ {1}𝑘 = 1)
282149, 281oveq12d 7449 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
283282adantr 480 . . . . . . 7 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵}𝑘 + Σ𝑘 ∈ {1}𝑘) = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
284278, 283eqtrd 2777 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {(𝐵 / ((2↑(𝐴 + 1)) − 1)), 𝐵, 1}𝑘 = (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1))
285204adantr 480 . . . . . 6 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝐵}𝑘 = ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
286263, 284, 2853brtr3d 5174 . . . . 5 ((𝜑𝐵 ≠ ((2↑(𝐴 + 1)) − 1)) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))))
287286ex 412 . . . 4 (𝜑 → (𝐵 ≠ ((2↑(𝐴 + 1)) − 1) → (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1)))))
288287necon1bd 2958 . . 3 (𝜑 → (¬ (((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) + 1) ≤ ((2↑(𝐴 + 1)) · (𝐵 / ((2↑(𝐴 + 1)) − 1))) → 𝐵 = ((2↑(𝐴 + 1)) − 1)))
289247, 288mpd 15 . 2 (𝜑𝐵 = ((2↑(𝐴 + 1)) − 1))
290242, 289jca 511 1 (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3o 1086   = wceq 1540  wcel 2108  wne 2940  wral 3061  {crab 3436  cun 3949  cin 3950  wss 3951  c0 4333  {csn 4626  {cpr 4628  {ctp 4630   class class class wbr 5143  cfv 6561  (class class class)co 7431  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  +crp 13034  ...cfz 13547  cexp 14102  Σcsu 15722  cdvds 16290   gcd cgcd 16531  cprime 16708  𝑐ccxp 26597   σ csgm 27139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-ef 16103  df-sin 16105  df-cos 16106  df-pi 16108  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-fbas 21361  df-fg 21362  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-perf 23145  df-cn 23235  df-cnp 23236  df-haus 23323  df-tx 23570  df-hmeo 23763  df-fil 23854  df-fm 23946  df-flim 23947  df-flf 23948  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-limc 25901  df-dv 25902  df-log 26598  df-cxp 26599  df-sgm 27145
This theorem is referenced by:  perfect  27275
  Copyright terms: Public domain W3C validator