ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  iseqf1olemab GIF version

Theorem iseqf1olemab 10475
Description: Lemma for seq3f1o 10490. (Contributed by Jim Kingdon, 27-Aug-2022.)
Hypotheses
Ref Expression
iseqf1olemqcl.k (𝜑𝐾 ∈ (𝑀...𝑁))
iseqf1olemqcl.j (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
iseqf1olemqcl.a (𝜑𝐴 ∈ (𝑀...𝑁))
iseqf1olemnab.b (𝜑𝐵 ∈ (𝑀...𝑁))
iseqf1olemnab.eq (𝜑 → (𝑄𝐴) = (𝑄𝐵))
iseqf1olemnab.q 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(𝐽𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽𝑢)))
iseqf1olemab.a (𝜑𝐴 ∈ (𝐾...(𝐽𝐾)))
iseqf1olemab.b (𝜑𝐵 ∈ (𝐾...(𝐽𝐾)))
Assertion
Ref Expression
iseqf1olemab (𝜑𝐴 = 𝐵)
Distinct variable groups:   𝑢,𝐴   𝑢,𝐵   𝑢,𝐽   𝑢,𝐾   𝑢,𝑀   𝑢,𝑁
Allowed substitution hints:   𝜑(𝑢)   𝑄(𝑢)

Proof of Theorem iseqf1olemab
StepHypRef Expression
1 eqtr3 2197 . . . . 5 ((𝐵 = 𝐾𝐴 = 𝐾) → 𝐵 = 𝐴)
21eqcomd 2183 . . . 4 ((𝐵 = 𝐾𝐴 = 𝐾) → 𝐴 = 𝐵)
32adantll 476 . . 3 (((𝜑𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐵)
4 iseqf1olemqcl.a . . . . . . . 8 (𝜑𝐴 ∈ (𝑀...𝑁))
5 elfzelz 10011 . . . . . . . 8 (𝐴 ∈ (𝑀...𝑁) → 𝐴 ∈ ℤ)
64, 5syl 14 . . . . . . 7 (𝜑𝐴 ∈ ℤ)
76zred 9364 . . . . . 6 (𝜑𝐴 ∈ ℝ)
87ltm1d 8878 . . . . 5 (𝜑 → (𝐴 − 1) < 𝐴)
98ad2antrr 488 . . . 4 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) < 𝐴)
107ad2antrr 488 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℝ)
11 peano2rem 8214 . . . . . 6 (𝐴 ∈ ℝ → (𝐴 − 1) ∈ ℝ)
1210, 11syl 14 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ ℝ)
13 iseqf1olemab.a . . . . . . . 8 (𝜑𝐴 ∈ (𝐾...(𝐽𝐾)))
14 elfzle2 10014 . . . . . . . 8 (𝐴 ∈ (𝐾...(𝐽𝐾)) → 𝐴 ≤ (𝐽𝐾))
1513, 14syl 14 . . . . . . 7 (𝜑𝐴 ≤ (𝐽𝐾))
1615ad2antrr 488 . . . . . 6 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ≤ (𝐽𝐾))
17 iseqf1olemqcl.k . . . . . . . . . . . 12 (𝜑𝐾 ∈ (𝑀...𝑁))
18 iseqf1olemqcl.j . . . . . . . . . . . 12 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
19 iseqf1olemnab.q . . . . . . . . . . . 12 𝑄 = (𝑢 ∈ (𝑀...𝑁) ↦ if(𝑢 ∈ (𝐾...(𝐽𝐾)), if(𝑢 = 𝐾, 𝐾, (𝐽‘(𝑢 − 1))), (𝐽𝑢)))
2017, 18, 4, 19iseqf1olemqval 10473 . . . . . . . . . . 11 (𝜑 → (𝑄𝐴) = if(𝐴 ∈ (𝐾...(𝐽𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽𝐴)))
2113iftrued 3541 . . . . . . . . . . 11 (𝜑 → if(𝐴 ∈ (𝐾...(𝐽𝐾)), if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))), (𝐽𝐴)) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
2220, 21eqtrd 2210 . . . . . . . . . 10 (𝜑 → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
2322ad2antrr 488 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
24 iseqf1olemnab.eq . . . . . . . . . . 11 (𝜑 → (𝑄𝐴) = (𝑄𝐵))
2524ad2antrr 488 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝑄𝐵))
26 iseqf1olemnab.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝑀...𝑁))
2717, 18, 26, 19iseqf1olemqval 10473 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐵) = if(𝐵 ∈ (𝐾...(𝐽𝐾)), if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))), (𝐽𝐵)))
28 iseqf1olemab.b . . . . . . . . . . . . . 14 (𝜑𝐵 ∈ (𝐾...(𝐽𝐾)))
2928iftrued 3541 . . . . . . . . . . . . 13 (𝜑 → if(𝐵 ∈ (𝐾...(𝐽𝐾)), if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))), (𝐽𝐵)) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
3027, 29eqtrd 2210 . . . . . . . . . . . 12 (𝜑 → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
3130ad2antrr 488 . . . . . . . . . . 11 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
32 simplr 528 . . . . . . . . . . . 12 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐵 = 𝐾)
3332iftrued 3541 . . . . . . . . . . 11 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = 𝐾)
3431, 33eqtrd 2210 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = 𝐾)
3525, 34eqtrd 2210 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = 𝐾)
36 simpr 110 . . . . . . . . . 10 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
3736iffalsed 3544 . . . . . . . . 9 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = (𝐽‘(𝐴 − 1)))
3823, 35, 373eqtr3d 2218 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐾 = (𝐽‘(𝐴 − 1)))
3938fveq2d 5515 . . . . . . 7 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐽‘(𝐽‘(𝐴 − 1))))
4018ad2antrr 488 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
41 elfzel1 10010 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
4217, 41syl 14 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℤ)
43 elfzel2 10009 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ ℤ)
4417, 43syl 14 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℤ)
45 peano2zm 9280 . . . . . . . . . . . . 13 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
466, 45syl 14 . . . . . . . . . . . 12 (𝜑 → (𝐴 − 1) ∈ ℤ)
4742, 44, 463jca 1177 . . . . . . . . . . 11 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ))
4847adantr 276 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ))
4942zred 9364 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℝ)
5049adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀 ∈ ℝ)
51 elfzelz 10011 . . . . . . . . . . . . . . 15 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)
5217, 51syl 14 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ ℤ)
5352zred 9364 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℝ)
5453adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 ∈ ℝ)
5546zred 9364 . . . . . . . . . . . . 13 (𝜑 → (𝐴 − 1) ∈ ℝ)
5655adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ ℝ)
57 elfzle1 10013 . . . . . . . . . . . . . 14 (𝐾 ∈ (𝑀...𝑁) → 𝑀𝐾)
5817, 57syl 14 . . . . . . . . . . . . 13 (𝜑𝑀𝐾)
5958adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀𝐾)
60 simpr 110 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
61 eqcom 2179 . . . . . . . . . . . . . . 15 (𝐴 = 𝐾𝐾 = 𝐴)
6260, 61sylnib 676 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐾 = 𝐴)
63 elfzle1 10013 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ (𝐾...(𝐽𝐾)) → 𝐾𝐴)
6413, 63syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐴)
65 zleloe 9289 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐾𝐴 ↔ (𝐾 < 𝐴𝐾 = 𝐴)))
6652, 6, 65syl2anc 411 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾𝐴 ↔ (𝐾 < 𝐴𝐾 = 𝐴)))
6764, 66mpbid 147 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 < 𝐴𝐾 = 𝐴))
6867adantr 276 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐾 < 𝐴𝐾 = 𝐴))
6962, 68ecased 1349 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 < 𝐴)
70 zltlem1 9299 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7152, 6, 70syl2anc 411 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7271adantr 276 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐾 < 𝐴𝐾 ≤ (𝐴 − 1)))
7369, 72mpbid 147 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐾 ≤ (𝐴 − 1))
7450, 54, 56, 59, 73letrd 8071 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑀 ≤ (𝐴 − 1))
757adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℝ)
7644zred 9364 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ ℝ)
7776adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝑁 ∈ ℝ)
7875lem1d 8879 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ≤ 𝐴)
79 elfzle2 10014 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝑀...𝑁) → 𝐴𝑁)
804, 79syl 14 . . . . . . . . . . . . 13 (𝜑𝐴𝑁)
8180adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → 𝐴𝑁)
8256, 75, 77, 78, 81letrd 8071 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ≤ 𝑁)
8374, 82jca 306 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝑀 ≤ (𝐴 − 1) ∧ (𝐴 − 1) ≤ 𝑁))
84 elfz2 10002 . . . . . . . . . 10 ((𝐴 − 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐴 − 1) ∈ ℤ) ∧ (𝑀 ≤ (𝐴 − 1) ∧ (𝐴 − 1) ≤ 𝑁)))
8548, 83, 84sylanbrc 417 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
8685adantlr 477 . . . . . . . 8 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
87 f1ocnvfv1 5772 . . . . . . . 8 ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐴 − 1) ∈ (𝑀...𝑁)) → (𝐽‘(𝐽‘(𝐴 − 1))) = (𝐴 − 1))
8840, 86, 87syl2anc 411 . . . . . . 7 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽‘(𝐽‘(𝐴 − 1))) = (𝐴 − 1))
8939, 88eqtrd 2210 . . . . . 6 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐴 − 1))
9016, 89breqtrd 4026 . . . . 5 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ≤ (𝐴 − 1))
9110, 12, 90lensymd 8069 . . . 4 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ (𝐴 − 1) < 𝐴)
929, 91pm2.21dd 620 . . 3 (((𝜑𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 = 𝐵)
93 zdceq 9317 . . . . . 6 ((𝐴 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝐴 = 𝐾)
946, 52, 93syl2anc 411 . . . . 5 (𝜑DECID 𝐴 = 𝐾)
95 exmiddc 836 . . . . 5 (DECID 𝐴 = 𝐾 → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
9694, 95syl 14 . . . 4 (𝜑 → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
9796adantr 276 . . 3 ((𝜑𝐵 = 𝐾) → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
983, 92, 97mpjaodan 798 . 2 ((𝜑𝐵 = 𝐾) → 𝐴 = 𝐵)
99 elfzelz 10011 . . . . . . . 8 (𝐵 ∈ (𝑀...𝑁) → 𝐵 ∈ ℤ)
10026, 99syl 14 . . . . . . 7 (𝜑𝐵 ∈ ℤ)
101100zred 9364 . . . . . 6 (𝜑𝐵 ∈ ℝ)
102101ltm1d 8878 . . . . 5 (𝜑 → (𝐵 − 1) < 𝐵)
103102ad2antrr 488 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) < 𝐵)
104101ad2antrr 488 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ∈ ℝ)
105 peano2rem 8214 . . . . . 6 (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
106104, 105syl 14 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) ∈ ℝ)
107 elfzle2 10014 . . . . . . . 8 (𝐵 ∈ (𝐾...(𝐽𝐾)) → 𝐵 ≤ (𝐽𝐾))
10828, 107syl 14 . . . . . . 7 (𝜑𝐵 ≤ (𝐽𝐾))
109108ad2antrr 488 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ≤ (𝐽𝐾))
11030ad2antrr 488 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
11124eqcomd 2183 . . . . . . . . . . 11 (𝜑 → (𝑄𝐵) = (𝑄𝐴))
112111ad2antrr 488 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = (𝑄𝐴))
11322ad2antrr 488 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
114 simpr 110 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐾)
115114iftrued 3541 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = 𝐾)
116113, 115eqtrd 2210 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐴) = 𝐾)
117112, 116eqtrd 2210 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝑄𝐵) = 𝐾)
118 simplr 528 . . . . . . . . . 10 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → ¬ 𝐵 = 𝐾)
119118iffalsed 3544 . . . . . . . . 9 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = (𝐽‘(𝐵 − 1)))
120110, 117, 1193eqtr3d 2218 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐾 = (𝐽‘(𝐵 − 1)))
121120fveq2d 5515 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐽‘(𝐽‘(𝐵 − 1))))
12218ad2antrr 488 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
123 peano2zm 9280 . . . . . . . . . . . . 13 (𝐵 ∈ ℤ → (𝐵 − 1) ∈ ℤ)
124100, 123syl 14 . . . . . . . . . . . 12 (𝜑 → (𝐵 − 1) ∈ ℤ)
12542, 44, 1243jca 1177 . . . . . . . . . . 11 (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ))
126125adantr 276 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ))
12749adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀 ∈ ℝ)
12853adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 ∈ ℝ)
129101, 105syl 14 . . . . . . . . . . . . 13 (𝜑 → (𝐵 − 1) ∈ ℝ)
130129adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ∈ ℝ)
13158adantr 276 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀𝐾)
132 simpr 110 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → ¬ 𝐵 = 𝐾)
133 eqcom 2179 . . . . . . . . . . . . . . 15 (𝐵 = 𝐾𝐾 = 𝐵)
134132, 133sylnib 676 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → ¬ 𝐾 = 𝐵)
135 elfzle1 10013 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (𝐾...(𝐽𝐾)) → 𝐾𝐵)
13628, 135syl 14 . . . . . . . . . . . . . . . 16 (𝜑𝐾𝐵)
137136adantr 276 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾𝐵)
138 zleloe 9289 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
13952, 100, 138syl2anc 411 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
140139adantr 276 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾𝐵 ↔ (𝐾 < 𝐵𝐾 = 𝐵)))
141137, 140mpbid 147 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾 < 𝐵𝐾 = 𝐵))
142134, 141ecased 1349 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 < 𝐵)
143 zltlem1 9299 . . . . . . . . . . . . . . 15 ((𝐾 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
14452, 100, 143syl2anc 411 . . . . . . . . . . . . . 14 (𝜑 → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
145144adantr 276 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐾 < 𝐵𝐾 ≤ (𝐵 − 1)))
146142, 145mpbid 147 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐾 ≤ (𝐵 − 1))
147127, 128, 130, 131, 146letrd 8071 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝑀 ≤ (𝐵 − 1))
148101lem1d 8879 . . . . . . . . . . . . 13 (𝜑 → (𝐵 − 1) ≤ 𝐵)
149 elfzle2 10014 . . . . . . . . . . . . . 14 (𝐵 ∈ (𝑀...𝑁) → 𝐵𝑁)
15026, 149syl 14 . . . . . . . . . . . . 13 (𝜑𝐵𝑁)
151129, 101, 76, 148, 150letrd 8071 . . . . . . . . . . . 12 (𝜑 → (𝐵 − 1) ≤ 𝑁)
152151adantr 276 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ≤ 𝑁)
153147, 152jca 306 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝑀 ≤ (𝐵 − 1) ∧ (𝐵 − 1) ≤ 𝑁))
154 elfz2 10002 . . . . . . . . . 10 ((𝐵 − 1) ∈ (𝑀...𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐵 − 1) ∈ ℤ) ∧ (𝑀 ≤ (𝐵 − 1) ∧ (𝐵 − 1) ≤ 𝑁)))
155126, 153, 154sylanbrc 417 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
156155adantr 276 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
157 f1ocnvfv1 5772 . . . . . . . 8 ((𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) ∧ (𝐵 − 1) ∈ (𝑀...𝑁)) → (𝐽‘(𝐽‘(𝐵 − 1))) = (𝐵 − 1))
158122, 156, 157syl2anc 411 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽‘(𝐽‘(𝐵 − 1))) = (𝐵 − 1))
159121, 158eqtrd 2210 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → (𝐽𝐾) = (𝐵 − 1))
160109, 159breqtrd 4026 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐵 ≤ (𝐵 − 1))
161104, 106, 160lensymd 8069 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → ¬ (𝐵 − 1) < 𝐵)
162103, 161pm2.21dd 620 . . 3 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ 𝐴 = 𝐾) → 𝐴 = 𝐵)
1636zcnd 9365 . . . . 5 (𝜑𝐴 ∈ ℂ)
164163ad2antrr 488 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 ∈ ℂ)
165100zcnd 9365 . . . . 5 (𝜑𝐵 ∈ ℂ)
166165ad2antrr 488 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐵 ∈ ℂ)
167 1cnd 7964 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 1 ∈ ℂ)
16824ad2antrr 488 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝑄𝐵))
16922ad2antrr 488 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))))
170 simpr 110 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐴 = 𝐾)
171170iffalsed 3544 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐴 = 𝐾, 𝐾, (𝐽‘(𝐴 − 1))) = (𝐽‘(𝐴 − 1)))
172169, 171eqtrd 2210 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐴) = (𝐽‘(𝐴 − 1)))
17330ad2antrr 488 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))))
174 simplr 528 . . . . . . . 8 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ¬ 𝐵 = 𝐾)
175174iffalsed 3544 . . . . . . 7 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → if(𝐵 = 𝐾, 𝐾, (𝐽‘(𝐵 − 1))) = (𝐽‘(𝐵 − 1)))
176173, 175eqtrd 2210 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝑄𝐵) = (𝐽‘(𝐵 − 1)))
177168, 172, 1763eqtr3d 2218 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)))
178 f1of1 5456 . . . . . . . 8 (𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁) → 𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
17918, 178syl 14 . . . . . . 7 (𝜑𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
180179ad2antrr 488 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁))
18185adantlr 477 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) ∈ (𝑀...𝑁))
182155adantr 276 . . . . . 6 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐵 − 1) ∈ (𝑀...𝑁))
183 f1veqaeq 5764 . . . . . 6 ((𝐽:(𝑀...𝑁)–1-1→(𝑀...𝑁) ∧ ((𝐴 − 1) ∈ (𝑀...𝑁) ∧ (𝐵 − 1) ∈ (𝑀...𝑁))) → ((𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)) → (𝐴 − 1) = (𝐵 − 1)))
184180, 181, 182, 183syl12anc 1236 . . . . 5 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → ((𝐽‘(𝐴 − 1)) = (𝐽‘(𝐵 − 1)) → (𝐴 − 1) = (𝐵 − 1)))
185177, 184mpd 13 . . . 4 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → (𝐴 − 1) = (𝐵 − 1))
186164, 166, 167, 185subcan2d 8300 . . 3 (((𝜑 ∧ ¬ 𝐵 = 𝐾) ∧ ¬ 𝐴 = 𝐾) → 𝐴 = 𝐵)
18796adantr 276 . . 3 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → (𝐴 = 𝐾 ∨ ¬ 𝐴 = 𝐾))
188162, 186, 187mpjaodan 798 . 2 ((𝜑 ∧ ¬ 𝐵 = 𝐾) → 𝐴 = 𝐵)
189 zdceq 9317 . . . 4 ((𝐵 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝐵 = 𝐾)
190100, 52, 189syl2anc 411 . . 3 (𝜑DECID 𝐵 = 𝐾)
191 exmiddc 836 . . 3 (DECID 𝐵 = 𝐾 → (𝐵 = 𝐾 ∨ ¬ 𝐵 = 𝐾))
192190, 191syl 14 . 2 (𝜑 → (𝐵 = 𝐾 ∨ ¬ 𝐵 = 𝐾))
19398, 188, 192mpjaodan 798 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978   = wceq 1353  wcel 2148  ifcif 3534   class class class wbr 4000  cmpt 4061  ccnv 4622  1-1wf1 5209  1-1-ontowf1o 5211  cfv 5212  (class class class)co 5869  cc 7800  cr 7801  1c1 7803   < clt 7982  cle 7983  cmin 8118  cz 9242  ...cfz 9995
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-addcom 7902  ax-addass 7904  ax-distr 7906  ax-i2m1 7907  ax-0lt1 7908  ax-0id 7910  ax-rnegex 7911  ax-cnre 7913  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-ltadd 7918
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-sub 8120  df-neg 8121  df-inn 8909  df-n0 9166  df-z 9243  df-uz 9518  df-fz 9996
This theorem is referenced by:  iseqf1olemmo  10478
  Copyright terms: Public domain W3C validator