Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bgoldbtbndlem2 Structured version   Visualization version   GIF version

Theorem bgoldbtbndlem2 42204
Description: Lemma 2 for bgoldbtbnd 42207. (Contributed by AV, 1-Aug-2020.)
Hypotheses
Ref Expression
bgoldbtbnd.m (𝜑𝑀 ∈ (ℤ11))
bgoldbtbnd.n (𝜑𝑁 ∈ (ℤ11))
bgoldbtbnd.b (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven ))
bgoldbtbnd.d (𝜑𝐷 ∈ (ℤ‘3))
bgoldbtbnd.f (𝜑𝐹 ∈ (RePart‘𝐷))
bgoldbtbnd.i (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))))
bgoldbtbnd.0 (𝜑 → (𝐹‘0) = 7)
bgoldbtbnd.1 (𝜑 → (𝐹‘1) = 13)
bgoldbtbnd.l (𝜑𝑀 < (𝐹𝐷))
bgoldbtbndlem2.s 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1)))
Assertion
Ref Expression
bgoldbtbndlem2 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))
Distinct variable groups:   𝐷,𝑖   𝑖,𝐹   𝑖,𝐼   𝑖,𝑁
Allowed substitution hints:   𝜑(𝑖,𝑛)   𝐷(𝑛)   𝑆(𝑖,𝑛)   𝐹(𝑛)   𝐼(𝑛)   𝑀(𝑖,𝑛)   𝑁(𝑛)   𝑋(𝑖,𝑛)

Proof of Theorem bgoldbtbndlem2
StepHypRef Expression
1 bgoldbtbnd.i . . . . 5 (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))))
2 elfzoelz 12664 . . . . . . 7 (𝐼 ∈ (1..^𝐷) → 𝐼 ∈ ℤ)
3 elfzoel2 12663 . . . . . . 7 (𝐼 ∈ (1..^𝐷) → 𝐷 ∈ ℤ)
4 elfzom1b 12761 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐼 ∈ (1..^𝐷) ↔ (𝐼 − 1) ∈ (0..^(𝐷 − 1))))
5 fzossrbm1 12691 . . . . . . . . . . 11 (𝐷 ∈ ℤ → (0..^(𝐷 − 1)) ⊆ (0..^𝐷))
65adantl 473 . . . . . . . . . 10 ((𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (0..^(𝐷 − 1)) ⊆ (0..^𝐷))
76sseld 3743 . . . . . . . . 9 ((𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐼 − 1) ∈ (0..^(𝐷 − 1)) → (𝐼 − 1) ∈ (0..^𝐷)))
84, 7sylbid 230 . . . . . . . 8 ((𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐼 ∈ (1..^𝐷) → (𝐼 − 1) ∈ (0..^𝐷)))
98com12 32 . . . . . . 7 (𝐼 ∈ (1..^𝐷) → ((𝐼 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐼 − 1) ∈ (0..^𝐷)))
102, 3, 9mp2and 717 . . . . . 6 (𝐼 ∈ (1..^𝐷) → (𝐼 − 1) ∈ (0..^𝐷))
11 fveq2 6352 . . . . . . . . 9 (𝑖 = (𝐼 − 1) → (𝐹𝑖) = (𝐹‘(𝐼 − 1)))
1211eleq1d 2824 . . . . . . . 8 (𝑖 = (𝐼 − 1) → ((𝐹𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2})))
13 oveq1 6820 . . . . . . . . . . 11 (𝑖 = (𝐼 − 1) → (𝑖 + 1) = ((𝐼 − 1) + 1))
1413fveq2d 6356 . . . . . . . . . 10 (𝑖 = (𝐼 − 1) → (𝐹‘(𝑖 + 1)) = (𝐹‘((𝐼 − 1) + 1)))
1514, 11oveq12d 6831 . . . . . . . . 9 (𝑖 = (𝐼 − 1) → ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) = ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))
1615breq1d 4814 . . . . . . . 8 (𝑖 = (𝐼 − 1) → (((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ↔ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)))
1715breq2d 4816 . . . . . . . 8 (𝑖 = (𝐼 − 1) → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) ↔ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))))
1812, 16, 173anbi123d 1548 . . . . . . 7 (𝑖 = (𝐼 − 1) → (((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) ↔ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))))
1918rspcv 3445 . . . . . 6 ((𝐼 − 1) ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))))
2010, 19syl 17 . . . . 5 (𝐼 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))))
211, 20syl5com 31 . . . 4 (𝜑 → (𝐼 ∈ (1..^𝐷) → ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))))
2221a1d 25 . . 3 (𝜑 → (𝑋 ∈ Odd → (𝐼 ∈ (1..^𝐷) → ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))))))
23223imp 1102 . 2 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))))
24 bgoldbtbndlem2.s . . . . 5 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1)))
25 simp2 1132 . . . . . . . 8 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 𝑋 ∈ Odd )
26 oddprmALTV 42108 . . . . . . . . 9 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → (𝐹‘(𝐼 − 1)) ∈ Odd )
27263ad2ant1 1128 . . . . . . . 8 (((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))) → (𝐹‘(𝐼 − 1)) ∈ Odd )
2825, 27anim12i 591 . . . . . . 7 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → (𝑋 ∈ Odd ∧ (𝐹‘(𝐼 − 1)) ∈ Odd ))
2928adantr 472 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝑋 ∈ Odd ∧ (𝐹‘(𝐼 − 1)) ∈ Odd ))
30 omoeALTV 42106 . . . . . 6 ((𝑋 ∈ Odd ∧ (𝐹‘(𝐼 − 1)) ∈ Odd ) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ Even )
3129, 30syl 17 . . . . 5 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ Even )
3224, 31syl5eqel 2843 . . . 4 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 𝑆 ∈ Even )
332zcnd 11675 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ (1..^𝐷) → 𝐼 ∈ ℂ)
34333ad2ant3 1130 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 𝐼 ∈ ℂ)
35 npcan1 10647 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ ℂ → ((𝐼 − 1) + 1) = 𝐼)
3634, 35syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐼 − 1) + 1) = 𝐼)
3736fveq2d 6356 . . . . . . . . . . . . . . . . 17 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝐹‘((𝐼 − 1) + 1)) = (𝐹𝐼))
3837oveq1d 6828 . . . . . . . . . . . . . . . 16 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) = ((𝐹𝐼) − (𝐹‘(𝐼 − 1))))
3938breq1d 4814 . . . . . . . . . . . . . . 15 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ↔ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)))
4039adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ (𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2})) → (((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ↔ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)))
41 eldifi 3875 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → (𝐹‘(𝐼 − 1)) ∈ ℙ)
42 prmz 15591 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐼 − 1)) ∈ ℙ → (𝐹‘(𝐼 − 1)) ∈ ℤ)
43 zre 11573 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝐼 − 1)) ∈ ℤ → (𝐹‘(𝐼 − 1)) ∈ ℝ)
44 simp1 1131 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → (𝐹𝑖) ∈ (ℙ ∖ {2}))
4544ralimi 3090 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → ∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}))
46 fzo0ss1 12692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1..^𝐷) ⊆ (0..^𝐷)
4746sseli 3740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐼 ∈ (1..^𝐷) → 𝐼 ∈ (0..^𝐷))
4847adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝐼 ∈ (1..^𝐷)) → 𝐼 ∈ (0..^𝐷))
49 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 = 𝐼 → (𝐹𝑖) = (𝐹𝐼))
5049eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 = 𝐼 → ((𝐹𝑖) ∈ (ℙ ∖ {2}) ↔ (𝐹𝐼) ∈ (ℙ ∖ {2})))
5150rspcv 3445 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐼 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝐹𝐼) ∈ (ℙ ∖ {2})))
5248, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐼 ∈ (1..^𝐷)) → (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝐹𝐼) ∈ (ℙ ∖ {2})))
5352ex 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐼 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝐹𝐼) ∈ (ℙ ∖ {2}))))
5453com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ (ℙ ∖ {2}))))
5554a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 ∈ Odd → (𝜑 → (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ (ℙ ∖ {2})))))
5655com13 88 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑖 ∈ (0..^𝐷)(𝐹𝑖) ∈ (ℙ ∖ {2}) → (𝜑 → (𝑋 ∈ Odd → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ (ℙ ∖ {2})))))
5745, 56syl 17 . . . . . . . . . . . . . . . . . . . 20 (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → (𝜑 → (𝑋 ∈ Odd → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ (ℙ ∖ {2})))))
581, 57mpcom 38 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ Odd → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ (ℙ ∖ {2}))))
59583imp 1102 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝐹𝐼) ∈ (ℙ ∖ {2}))
60 eldifi 3875 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐼) ∈ (ℙ ∖ {2}) → (𝐹𝐼) ∈ ℙ)
61 prmz 15591 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐼) ∈ ℙ → (𝐹𝐼) ∈ ℤ)
62 zre 11573 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝐼) ∈ ℤ → (𝐹𝐼) ∈ ℝ)
63 bgoldbtbnd.n . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑁 ∈ (ℤ11))
64 eluzelz 11889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ (ℤ11) → 𝑁 ∈ ℤ)
65 zre 11573 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
66 oddz 42054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 ∈ Odd → 𝑋 ∈ ℤ)
6766zred 11674 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑋 ∈ Odd → 𝑋 ∈ ℝ)
68 simplr 809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → 𝑋 ∈ ℝ)
69 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝐹𝐼) ∈ ℝ)
70 4re 11289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 4 ∈ ℝ
7170a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → 4 ∈ ℝ)
7268, 69, 71lesubaddd 10816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → ((𝑋 − (𝐹𝐼)) ≤ 4 ↔ 𝑋 ≤ (4 + (𝐹𝐼))))
73 simpllr 817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → 𝑋 ∈ ℝ)
74 simplrr 820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (𝐹‘(𝐼 − 1)) ∈ ℝ)
7573, 74resubcld 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ ℝ)
7670a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → 4 ∈ ℝ)
77 simplrl 819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (𝐹𝐼) ∈ ℝ)
7876, 77readdcld 10261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (4 + (𝐹𝐼)) ∈ ℝ)
7978, 74resubcld 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))) ∈ ℝ)
80 simplll 815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → 𝑁 ∈ ℝ)
8171, 69readdcld 10261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (4 + (𝐹𝐼)) ∈ ℝ)
82 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝐹‘(𝐼 − 1)) ∈ ℝ)
8368, 81, 82lesub1d 10826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝑋 ≤ (4 + (𝐹𝐼)) ↔ (𝑋 − (𝐹‘(𝐼 − 1))) ≤ ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1)))))
8483biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ 𝑋 ≤ (4 + (𝐹𝐼))) → (𝑋 − (𝐹‘(𝐼 − 1))) ≤ ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))))
8584adantrr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (𝑋 − (𝐹‘(𝐼 − 1))) ≤ ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))))
86 resubcl 10537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ) → ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ∈ ℝ)
8786adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ∈ ℝ)
88 simpll 807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → 𝑁 ∈ ℝ)
89 ltaddsub2 10695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((4 ∈ ℝ ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁 ↔ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)))
9089bicomd 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((4 ∈ ℝ ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ↔ (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
9171, 87, 88, 90syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ↔ (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
9291biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
9392adantld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → ((𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)) → (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
9493imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁)
95 4cn 11290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 4 ∈ ℂ
9695a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → 4 ∈ ℂ)
9769recnd 10260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝐹𝐼) ∈ ℂ)
98 recn 10218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐹‘(𝐼 − 1)) ∈ ℝ → (𝐹‘(𝐼 − 1)) ∈ ℂ)
9998adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ) → (𝐹‘(𝐼 − 1)) ∈ ℂ)
10099adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝐹‘(𝐼 − 1)) ∈ ℂ)
10196, 97, 100addsubassd 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))) = (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))))
102101breq1d 4814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))) < 𝑁 ↔ (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
103102adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))) < 𝑁 ↔ (4 + ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))) < 𝑁))
10494, 103mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → ((4 + (𝐹𝐼)) − (𝐹‘(𝐼 − 1))) < 𝑁)
10575, 79, 80, 85, 104lelttrd 10387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) ∧ (𝑋 ≤ (4 + (𝐹𝐼)) ∧ ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4))) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)
106105exp32 632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (𝑋 ≤ (4 + (𝐹𝐼)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
10772, 106sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
108107com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) ∧ ((𝐹𝐼) ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
109108exp32 632 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 ∈ ℝ ∧ 𝑋 ∈ ℝ) → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
11067, 109sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑁 ∈ ℝ ∧ 𝑋 ∈ Odd ) → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
111110ex 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℝ → (𝑋 ∈ Odd → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))))
11265, 111syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℤ → (𝑋 ∈ Odd → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))))
11363, 64, 1123syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ Odd → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))))
114113imp 444 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑋 ∈ Odd ) → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
1151143adant3 1127 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹𝐼) ∈ ℝ → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
11662, 115syl5com 31 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐼) ∈ ℤ → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
11760, 61, 1163syl 18 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐼) ∈ (ℙ ∖ {2}) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))))
11859, 117mpcom 38 . . . . . . . . . . . . . . . . 17 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘(𝐼 − 1)) ∈ ℝ → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))
11943, 118syl5com 31 . . . . . . . . . . . . . . . 16 ((𝐹‘(𝐼 − 1)) ∈ ℤ → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))
12041, 42, 1193syl 18 . . . . . . . . . . . . . . 15 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))
121120impcom 445 . . . . . . . . . . . . . 14 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ (𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2})) → (((𝐹𝐼) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
12240, 121sylbid 230 . . . . . . . . . . . . 13 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ (𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2})) → (((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
123122expcom 450 . . . . . . . . . . . 12 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))
124123com23 86 . . . . . . . . . . 11 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → (((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))))
125124imp 444 . . . . . . . . . 10 (((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4)) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
1261253adant3 1127 . . . . . . . . 9 (((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)))
127126impcom 445 . . . . . . . 8 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → ((𝑋 − (𝐹𝐼)) ≤ 4 → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))
128127com12 32 . . . . . . 7 ((𝑋 − (𝐹𝐼)) ≤ 4 → (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))
129128adantl 473 . . . . . 6 ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁))
130129impcom 445 . . . . 5 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝑋 − (𝐹‘(𝐼 − 1))) < 𝑁)
13124, 130syl5eqbr 4839 . . . 4 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 𝑆 < 𝑁)
13270a1i 11 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 4 ∈ ℝ)
133 1eluzge0 11925 . . . . . . . . . . . . . . . 16 1 ∈ (ℤ‘0)
134 fzoss1 12689 . . . . . . . . . . . . . . . 16 (1 ∈ (ℤ‘0) → (1..^𝐷) ⊆ (0..^𝐷))
135133, 134mp1i 13 . . . . . . . . . . . . . . 15 (𝜑 → (1..^𝐷) ⊆ (0..^𝐷))
136135sselda 3744 . . . . . . . . . . . . . 14 ((𝜑𝐼 ∈ (1..^𝐷)) → 𝐼 ∈ (0..^𝐷))
137 oveq1 6820 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝐼 → (𝑖 + 1) = (𝐼 + 1))
138137fveq2d 6356 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝐼 → (𝐹‘(𝑖 + 1)) = (𝐹‘(𝐼 + 1)))
139138, 49oveq12d 6831 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐼 → ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) = ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)))
140139breq1d 4814 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐼 → (((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ↔ ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)) < (𝑁 − 4)))
141139breq2d 4816 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐼 → (4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) ↔ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹𝐼))))
14250, 140, 1413anbi123d 1548 . . . . . . . . . . . . . . 15 (𝑖 = 𝐼 → (((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) ↔ ((𝐹𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)))))
143142rspcv 3445 . . . . . . . . . . . . . 14 (𝐼 ∈ (0..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → ((𝐹𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)))))
144136, 143syl 17 . . . . . . . . . . . . 13 ((𝜑𝐼 ∈ (1..^𝐷)) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → ((𝐹𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)))))
14561zred 11674 . . . . . . . . . . . . . . 15 ((𝐹𝐼) ∈ ℙ → (𝐹𝐼) ∈ ℝ)
14660, 145syl 17 . . . . . . . . . . . . . 14 ((𝐹𝐼) ∈ (ℙ ∖ {2}) → (𝐹𝐼) ∈ ℝ)
1471463ad2ant1 1128 . . . . . . . . . . . . 13 (((𝐹𝐼) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝐼 + 1)) − (𝐹𝐼)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝐼 + 1)) − (𝐹𝐼))) → (𝐹𝐼) ∈ ℝ)
148144, 147syl6 35 . . . . . . . . . . . 12 ((𝜑𝐼 ∈ (1..^𝐷)) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → (𝐹𝐼) ∈ ℝ))
149148ex 449 . . . . . . . . . . 11 (𝜑 → (𝐼 ∈ (1..^𝐷) → (∀𝑖 ∈ (0..^𝐷)((𝐹𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹𝑖))) → (𝐹𝐼) ∈ ℝ)))
1501, 149mpid 44 . . . . . . . . . 10 (𝜑 → (𝐼 ∈ (1..^𝐷) → (𝐹𝐼) ∈ ℝ))
151150imp 444 . . . . . . . . 9 ((𝜑𝐼 ∈ (1..^𝐷)) → (𝐹𝐼) ∈ ℝ)
1521513adant2 1126 . . . . . . . 8 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝐹𝐼) ∈ ℝ)
153152ad2antrr 764 . . . . . . 7 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝐹𝐼) ∈ ℝ)
15442zred 11674 . . . . . . . . . 10 ((𝐹‘(𝐼 − 1)) ∈ ℙ → (𝐹‘(𝐼 − 1)) ∈ ℝ)
15541, 154syl 17 . . . . . . . . 9 ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) → (𝐹‘(𝐼 − 1)) ∈ ℝ)
1561553ad2ant1 1128 . . . . . . . 8 (((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))) → (𝐹‘(𝐼 − 1)) ∈ ℝ)
157156ad2antlr 765 . . . . . . 7 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝐹‘(𝐼 − 1)) ∈ ℝ)
158153, 157resubcld 10650 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ∈ ℝ)
159673ad2ant2 1129 . . . . . . . 8 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 𝑋 ∈ ℝ)
160 resubcl 10537 . . . . . . . 8 ((𝑋 ∈ ℝ ∧ (𝐹‘(𝐼 − 1)) ∈ ℝ) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ ℝ)
161159, 156, 160syl2an 495 . . . . . . 7 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ ℝ)
162161adantr 472 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝑋 − (𝐹‘(𝐼 − 1))) ∈ ℝ)
16333, 35syl 17 . . . . . . . . . . . . . 14 (𝐼 ∈ (1..^𝐷) → ((𝐼 − 1) + 1) = 𝐼)
1641633ad2ant3 1130 . . . . . . . . . . . . 13 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐼 − 1) + 1) = 𝐼)
165164fveq2d 6356 . . . . . . . . . . . 12 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝐹‘((𝐼 − 1) + 1)) = (𝐹𝐼))
166165oveq1d 6828 . . . . . . . . . . 11 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) = ((𝐹𝐼) − (𝐹‘(𝐼 − 1))))
167166breq2d 4816 . . . . . . . . . 10 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) ↔ 4 < ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))))
168167biimpcd 239 . . . . . . . . 9 (4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 4 < ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))))
1691683ad2ant3 1130 . . . . . . . 8 (((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1)))) → ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → 4 < ((𝐹𝐼) − (𝐹‘(𝐼 − 1)))))
170169impcom 445 . . . . . . 7 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → 4 < ((𝐹𝐼) − (𝐹‘(𝐼 − 1))))
171170adantr 472 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 4 < ((𝐹𝐼) − (𝐹‘(𝐼 − 1))))
172159ad2antrr 764 . . . . . . 7 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 𝑋 ∈ ℝ)
173 bgoldbtbnd.d . . . . . . . . . . . . . . . . 17 (𝜑𝐷 ∈ (ℤ‘3))
174 eluzge3nn 11923 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ (ℤ‘3) → 𝐷 ∈ ℕ)
175173, 174syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℕ)
176175adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝐼 ∈ (1..^𝐷)) → 𝐷 ∈ ℕ)
177 bgoldbtbnd.f . . . . . . . . . . . . . . . 16 (𝜑𝐹 ∈ (RePart‘𝐷))
178177adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝐼 ∈ (1..^𝐷)) → 𝐹 ∈ (RePart‘𝐷))
179133, 134mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝐷 ∈ (ℤ‘3) → (1..^𝐷) ⊆ (0..^𝐷))
180 fzossfz 12682 . . . . . . . . . . . . . . . . . 18 (0..^𝐷) ⊆ (0...𝐷)
181179, 180syl6ss 3756 . . . . . . . . . . . . . . . . 17 (𝐷 ∈ (ℤ‘3) → (1..^𝐷) ⊆ (0...𝐷))
182173, 181syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1..^𝐷) ⊆ (0...𝐷))
183182sselda 3744 . . . . . . . . . . . . . . 15 ((𝜑𝐼 ∈ (1..^𝐷)) → 𝐼 ∈ (0...𝐷))
184176, 178, 183iccpartxr 41865 . . . . . . . . . . . . . 14 ((𝜑𝐼 ∈ (1..^𝐷)) → (𝐹𝐼) ∈ ℝ*)
185 fzofzp1 12759 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (0..^𝐷) → (𝐼 + 1) ∈ (0...𝐷))
186136, 185syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝐼 ∈ (1..^𝐷)) → (𝐼 + 1) ∈ (0...𝐷))
187176, 178, 186iccpartxr 41865 . . . . . . . . . . . . . 14 ((𝜑𝐼 ∈ (1..^𝐷)) → (𝐹‘(𝐼 + 1)) ∈ ℝ*)
188184, 187jca 555 . . . . . . . . . . . . 13 ((𝜑𝐼 ∈ (1..^𝐷)) → ((𝐹𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈ ℝ*))
1891883adant2 1126 . . . . . . . . . . . 12 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝐹𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈ ℝ*))
190 elico1 12411 . . . . . . . . . . . 12 (((𝐹𝐼) ∈ ℝ* ∧ (𝐹‘(𝐼 + 1)) ∈ ℝ*) → (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝐹𝐼) ≤ 𝑋𝑋 < (𝐹‘(𝐼 + 1)))))
191189, 190syl 17 . . . . . . . . . . 11 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝐹𝐼) ≤ 𝑋𝑋 < (𝐹‘(𝐼 + 1)))))
192 simp2 1132 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ (𝐹𝐼) ≤ 𝑋𝑋 < (𝐹‘(𝐼 + 1))) → (𝐹𝐼) ≤ 𝑋)
193191, 192syl6bi 243 . . . . . . . . . 10 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) → (𝐹𝐼) ≤ 𝑋))
194193adantrd 485 . . . . . . . . 9 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (𝐹𝐼) ≤ 𝑋))
195194adantr 472 . . . . . . . 8 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (𝐹𝐼) ≤ 𝑋))
196195imp 444 . . . . . . 7 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝐹𝐼) ≤ 𝑋)
197153, 172, 157, 196lesub1dd 10835 . . . . . 6 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → ((𝐹𝐼) − (𝐹‘(𝐼 − 1))) ≤ (𝑋 − (𝐹‘(𝐼 − 1))))
198132, 158, 162, 171, 197ltletrd 10389 . . . . 5 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 4 < (𝑋 − (𝐹‘(𝐼 − 1))))
199198, 24syl6breqr 4846 . . . 4 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → 4 < 𝑆)
20032, 131, 1993jca 1123 . . 3 ((((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) ∧ (𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4)) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))
201200ex 449 . 2 (((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) ∧ ((𝐹‘(𝐼 − 1)) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))) < (𝑁 − 4) ∧ 4 < ((𝐹‘((𝐼 − 1) + 1)) − (𝐹‘(𝐼 − 1))))) → ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))
20223, 201mpdan 705 1 ((𝜑𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  cdif 3712  wss 3715  {csn 4321   class class class wbr 4804  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131  *cxr 10265   < clt 10266  cle 10267  cmin 10458  cn 11212  2c2 11262  3c3 11263  4c4 11264  7c7 11267  cz 11569  cdc 11685  cuz 11879  [,)cico 12370  ...cfz 12519  ..^cfzo 12659  cprime 15587  RePartciccp 41859   Even ceven 42047   Odd codd 42048   GoldbachEven cgbe 42143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-ico 12374  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-dvds 15183  df-prm 15588  df-iccp 41860  df-even 42049  df-odd 42050
This theorem is referenced by:  bgoldbtbndlem4  42206
  Copyright terms: Public domain W3C validator